psigmaEquivSubtype — Mathlib

English

A PSigma over α with Prop fibers is equivalent to the subtype {x : α | P x}.

Русский

PSigma над α с волокнами Prop эквивалентна подтиповому множеству {x ∈ α | P x}.

LaTeX

$$$$ (\Sigma' i, P i) \cong Subtype(P). $$$$

Lean4

/-- A `PSigma` with `Prop` fibers is equivalent to the subtype. -/
def psigmaEquivSubtype {α : Type v} (P : α → Prop) : (Σ' i, P i) ≃ Subtype P
    where
  toFun x := ⟨x.1, x.2⟩
  invFun x := ⟨x.1, x.2⟩

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