subtypeProdEquivSigmaSubtype — Mathlib

English

A subtype of a product is equivalent to a dependent sigma type: { x : α × β // p x.1 x.2 } ≃ Σ a, { b : β // p a b }.

Русский

Подтип произведения эквивалентен зависимому сигма-типу: {x ∈ α×β | p x.1 x.2} ≃ Σ a, { b ∈ β | p a b }.

LaTeX

$$$\{ x : \alpha \times \beta \mid p(x.1, x.2) \} \simeq \Sigma a, \{ b : \beta \mid p(a,b) \}. $$$

Lean4

/-- A subtype of a `Prod` is equivalent to a sigma type whose fibers are subtypes. -/
def subtypeProdEquivSigmaSubtype {α β} (p : α → β → Prop) : { x : α × β // p x.1 x.2 } ≃ Σ a, { b : β // p a b }
    where
  toFun x := ⟨x.1.1, x.1.2, x.property⟩
  invFun x := ⟨⟨x.1, x.2⟩, x.2.property⟩

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