Trivial_Relation_is_Universally_Congruent

⚠️ Retired — incorrect formalization

The Lean statement below does not express the result Trivial_Relation_is_Universally_Congruent is named for, so its Proved status carries no information about it. Do not import it or use it as a dependency.

The trivial relation S × S on a set S is universally congruent with every closed operation on S.

Why this node was retired

The posted statement is

theorem Trivial_Relation_is_Universally_Congruent {α : Type _} [Mul α] (x₁ x₂ y₁ y₂ : α) : True → True := by sorry

The goal is True → True, closed by fun _ => trivial. The elements x₁ x₂ y₁ y₂ and the multiplication on α are never used, and no congruence property is stated.

What a faithful statement would require

The conclusion must state that the always-true relation is compatible with *, i.e. that it is a congruence on the magma.

No corrected replacement node exists yet.