to_submonoid_inj — Mathlib

English

Two congruences c and d satisfy c ≤ d if and only if their submonoids satisfy c.submonoid ≤ d.submonoid.

Русский

Две конгруэнции c и d удовлетворяют c ≤ d тогда и только тогда, когда их подподмножества удовлетворяют c.submonoid ≤ d.submonoid.

LaTeX

$$c ≤ d ↔ (c.submonoid) ≤ d.submonoid$$

Lean4

@[to_additive]
theorem to_submonoid_inj (c d : Con M) (H : (c : Submonoid (M × M)) = d) : c = d :=
  ext fun x y => show (x, y) ∈ c.submonoid ↔ (x, y) ∈ d from H ▸ Iff.rfl

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