setProdEquivSigma — Mathlib

English

There is a natural equivalence between a subset s of α × β and the sigma-type Σ x:α, {y:β | (x,y) ∈ s}.

Русский

Существует естественное эквивалентности между подмножеством s ⊆ α × β и сигма-типом Σ x:α, { y:β | (x,y) ∈ s }.

LaTeX

$$$ s \simeq \Sigma x: \alpha, \{ y: \beta \mid (x,y) \in s \} $$$

Lean4

/-- A set `s` in `α × β` is equivalent to the sigma-type `Σ x, {y | (x, y) ∈ s}`. -/
def setProdEquivSigma {α β : Type*} (s : Set (α × β)) : s ≃ Σ x : α, {y : β | (x, y) ∈ s}
    where
  toFun x := ⟨x.1.1, x.1.2, by simp⟩
  invFun x := ⟨(x.1, x.2.1), x.2.2⟩

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