univ_subtype — Mathlib

English

For any property p on a set A, the universal set of the subtype {x ∈ A | p(x)} equals the union over all x of the singleton {⟨x, h⟩} for proofs h of p(x).

Русский

Для свойств p на множестве A множество-подтип {x ∈ A | p(x)} образует единство по всем x и доказательствам p(x) каждого x: универсума подтипа равен объединению всех одиноких множеств {⟨x, h⟩}.

LaTeX

$$$(\text{univ} : Set(\operatorname{Subtype} p)) = \bigcup_{x} \bigcup_{h: p(x)} \{\langle x, h \rangle\}$$$

Lean4

theorem univ_subtype {p : α → Prop} : (univ : Set (Subtype p)) = ⋃ (x) (h : p x), {⟨x, h⟩} :=
  Set.ext fun ⟨x, h⟩ => by simp [h]

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