isOpen_sigma_fst_preimage — Mathlib

English

For any set s of indices, the preimage of s under Sigma.fst is open in the sum type.

Русский

Для любого множества индексов s обратное образ Sigma.fst(s) открыто в сумму.

LaTeX

$$$\\operatorname{IsOpen}(\\Sigma.fst^{-1} s)$$$

Lean4

theorem isOpen_sigma_fst_preimage (s : Set ι) : IsOpen (Sigma.fst ⁻¹' s : Set (Σ a, σ a)) :=
  by
  rw [← biUnion_of_singleton s, preimage_iUnion₂]
  simp only [← range_sigmaMk]
  exact isOpen_biUnion fun _ _ => isOpen_range_sigmaMk

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