sigmaSubtype — Mathlib

English

A subtype of a sigma that pins down the base of the sigma is equivalent to the fiber.

Русский

Подтип сигмы, фиксирующий основание сигмы, эквивалентен волокну.

LaTeX

$$$\\{ s : \\Sigma \\beta // s.1 = a \\} \\simeq \\beta a$$$

Lean4

/-- A subtype of a sigma which pins down the base of the sigma is equivalent to
the respective fiber. -/
@[simps]
def sigmaSubtype {α : Type*} {β : α → Type*} (a : α) : { s : Sigma β // s.1 = a } ≃ β a
    where
  toFun := fun ⟨⟨_, b⟩, h⟩ => h ▸ b
  invFun b := ⟨⟨a, b⟩, rfl⟩
  left_inv := fun ⟨a, h⟩ ↦ by cases h; simp
  right_inv b := by simp

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