English
The type of all functions with fixed values except at one point is equivalent to the codomain.
Русский
Тип всех функций с фиксированными значениями кроме одной точки эквивалентен кодомену.
LaTeX
$$def sigmaOptionEquivOfSome ... : (Σ x : Option α, p x) ≃ Σ x : α, p (some x)$$
Lean4
/-- The `Pi`-type `∀ i, π i` is equivalent to the type of sections `f : ι → Σ i, π i` of the
`Sigma` type such that for all `i` we have `(f i).fst = i`. -/
def piEquivSubtypeSigma (ι) (π : ι → Type*) : (∀ i, π i) ≃ { f : ι → Σ i, π i // ∀ i, (f i).1 = i }
where
toFun := fun f => ⟨fun i => ⟨i, f i⟩, fun _ => rfl⟩
invFun := fun f i => by rw [← f.2 i]; exact (f.1 i).2
right_inv := fun ⟨f, hf⟩ =>
Subtype.eq <| funext fun i => Sigma.eq (hf i).symm <| eq_of_heq <| rec_heq_of_heq _ <| by simp
