quotient_mk_sInf_eq — Mathlib

English

Two elements x and y of α map to the same quotient by sInf S iff x and y are related by every s ∈ S.

Русский

Два элемента x,y ∈ α равны в фактор-множество по sInf S тогда и только тогда, когда x и y связаны во всех s ∈ S.

LaTeX

$$$$ Quotient.mk (sInf S)\\ x = Quotient.mk (sInf S)\\ y \\iff \\forall s \\in S,\\ s x y. $$$$

Lean4

theorem quotient_mk_sInf_eq {S : Set (Setoid α)} {x y : α} :
    Quotient.mk (sInf S) x = Quotient.mk (sInf S) y ↔ ∀ s ∈ S, s x y := by simp [sInf_iff]

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