iSup_mk — Mathlib

English

If each s i is open, then the iSup of ⟨s i, h i⟩ equals ⟨⋃ i, s i, isOpen_iUnion h⟩.

Русский

Если каждый s_i открыто, то iSup над ⟨s_i, h_i⟩ равен ⟨⋃ i s_i, isOpen_iUnion h⟩.

LaTeX

$$$ (\iSup i, ⟨s_i, h_i⟩) = ⟨\bigcup_i s_i, isOpen_iUnion\, h \rangle $$$

Lean4

@[simp]
theorem iSup_mk {ι} (s : ι → Set α) (h : ∀ i, IsOpen (s i)) :
    (⨆ i, ⟨s i, h i⟩ : Opens α) = ⟨⋃ i, s i, isOpen_iUnion h⟩ :=
  iSup_def _

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