mem_part_ofSetoid_iff_rel — Mathlib

English

The function ofSetoid assigns to a Setoid s and a finite universe an induced finpartition of the universe into equivalence classes of s.

Русский

Функция ofSetoid задаёт для множества и множества классов эквивалентности разбиение на классы эквивалентности.

LaTeX

$$$\\text{ofSetoid}(s) : Finpartition(\\text{univ})$$$

Lean4

theorem mem_part_ofSetoid_iff_rel {s : Setoid α} [DecidableRel s.r] {b : α} : b ∈ (ofSetoid s).part a ↔ s a b :=
  by
  suffices b ∈ (ofSetSetoid s univ).part a ↔ a ∈ univ ∧ b ∈ univ ∧ s a b by simpa
  exact mem_part_ofSetSetoid_iff_rel univ

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