prodSubtypeFstEquivSubtypeProd — Mathlib

English

A subtype of a product depending only on the first component is equivalent to a product of the first subtype with the second type.

Русский

Подтип произведения, зависящий только от первой компоненты, эквивалентен произведению подтипа первой компоненты на вторую константную часть.

LaTeX

$$$\text{Equiv} \big(\{ (a,b) \mid p(a) \} \big) \cong \{ a \mid p(a) \} \times \beta.$$$

Lean4

/-- A subtype of a `Prod` that depends only on the first component is equivalent to the
corresponding subtype of the first type times the second type. -/
def prodSubtypeFstEquivSubtypeProd {α β} {p : α → Prop} : { s : α × β // p s.1 } ≃ { a // p a } × β
    where
  toFun x := ⟨⟨x.1.1, x.2⟩, x.1.2⟩
  invFun x := ⟨⟨x.1.1, x.2⟩, x.1.2⟩

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