conGen_of_con — Mathlib

English

Congruences are exactly their generated smallest containing congruence; conGen(c) = c.

Русский

Конгруэнции равны наименьшим конгруэнтным отношениям, в которых они содержатся; conGen(c) = c.

LaTeX

$$$conGen(c) = c$$$

Lean4

/-- Congruence relations equal the smallest congruence relation in which they are contained. -/
@[to_additive (attr := simp) addConGen_of_addCon /-- Additive congruence relations equal the
    smallest additive congruence relation in which they are contained. -/
    ]
theorem conGen_of_con (c : Con M) : conGen c = c :=
  le_antisymm (by rw [conGen_eq]; exact sInf_le fun _ _ => id) ConGen.Rel.of

Похожие утверждения