subtypeSigmaEquiv — Mathlib

English

A subtype of a sigma-type is equivalent to the sigma-type over a subtype.

Русский

Подтип сигма-типa эквивалентен сигма-типу над подтипом.

LaTeX

$$$\\{ y : \\Sigma x : \\alpha, p x \\;\\mid\\; q y.1 \\} \\simeq \\Sigma x : \\text{Subtype } q, p x.1$$$

Lean4

/-- A subtype of a sigma-type is a sigma-type over a subtype. -/
def subtypeSigmaEquiv {α} (p : α → Type v) (q : α → Prop) : { y : Sigma p // q y.1 } ≃ Σ x : Subtype q, p x.1 :=
  ⟨fun x => ⟨⟨x.1.1, x.2⟩, x.1.2⟩, fun x => ⟨⟨x.1.1, x.2⟩, x.1.2⟩, fun _ => rfl, fun _ => rfl⟩

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