ext — Mathlib

English

Two partitions are equal if and only if they have the same membership relation for every element.

Русский

Два разбиения равны тогда и только тогда, когда для каждого элемента выполняется одинаковость членства.

LaTeX

$$$\forall x, x \in P \iff x \in Q \Rightarrow P = Q$$$

Lean4

@[ext]
theorem ext {P Q : Partition s} (hP : ∀ x, x ∈ P ↔ x ∈ Q) : P = Q :=
  SetLike.ext hP

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