eq_of_mem_classes — Mathlib

English

If x lies in a class b and also in a class b' of the same partition with membership proofs, then b = b'.

Русский

Если x принадлежит классу b и классу b' разбиения, то b = b'.

LaTeX

$$Given a class membership of x in b and b', and H saying uniqueness, we conclude b = b'.$$

Lean4

/-- If x ∈ α is in 2 equivalence classes, the equivalence classes are equal. -/
theorem eq_of_mem_classes {r : Setoid α} {x b} (hc : b ∈ r.classes) (hb : x ∈ b) {b'} (hc' : b' ∈ r.classes)
    (hb' : x ∈ b') : b = b' :=
  eq_of_mem_eqv_class classes_eqv_classes hc hb hc' hb'

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