mem_coe — Mathlib

English

Membership of a pair in the coerced submonoid c.submonoid is equivalent to membership in the relation c itself: (x,y) ∈ (↑c) ↔ (x,y) ∈ c.

Русский

Принадлежность пары к скалярному подмонойду c.submonoid эквивалентна принадлежности пары к конгруэнции c: (x,y) ∈ ↑c ↔ (x,y) ∈ c.

LaTeX

$$(x,y) ∈ (↑c : Submonoid (M × M)) ↔ (x,y) ∈ c$$

Lean4

@[to_additive]
theorem mem_coe {c : Con M} {x y} : (x, y) ∈ (↑c : Submonoid (M × M)) ↔ (x, y) ∈ c :=
  Iff.rfl

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