apply — Mathlib

English

The supremum of applying a chain of continuous endomorphisms to a supremum equals the product of the supremum of a zip of chains.

Русский

Предел объединения применения цепи непрерывных отображений к верхнему пределу совпадает с верхним пределом произведения цепей.

LaTeX

$$$\omegaSup\,c_0\,(\omegaSup\,c_1) = \mathrm{Prod}.\ \mathrm{apply}\ (\omegaSup\,(c_0\,\mathrm{zip}\,c_1))$$$

Lean4

/-- The application of continuous functions as a continuous function. -/
@[simps]
def apply : (α →𝒄 β) × α →𝒄 β where
  toFun f := f.1 f.2
  monotone' x y
    h := by
    dsimp
    trans y.fst x.snd <;> [apply h.1; apply y.1.monotone h.2]
  map_ωSup'
    c := by
    apply le_antisymm
    · apply ωSup_le
      intro i
      dsimp
      rw [(c _).fst.continuous]
      apply ωSup_le
      intro j
      apply le_ωSup_of_le (max i j)
      apply apply_mono
      · exact monotone_fst (OrderHom.mono _ (le_max_left _ _))
      · exact monotone_snd (OrderHom.mono _ (le_max_right _ _))
    · apply ωSup_le
      intro i
      apply le_ωSup_of_le i
      dsimp
      apply OrderHom.mono _
      apply le_ωSup_of_le i
      rfl

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