equicontinuousWithinAt_iInf_dom — Mathlib

English

If hk is EquicontinuousWithinAt with t-dependence indexed by k, then EquicontinuousWithinAt with the iInf t is obtained.

Русский

Если hk непрерывно в точке по вкладке k, то эконтинуированность внутри iInf получаема.

LaTeX

$$$\\text{If } hk : EquicontinuousWithinAt(F,S,x_0)\\text{ for }t_k, \\text{ then } EquicontinuousWithinAt(F,S,x_0)\\text{ for }t := \\bigwedge_k t_k.$$$

Lean4

theorem equicontinuousWithinAt_iInf_dom {t : κ → TopologicalSpace X'} {F : ι → X' → α} {S : Set X'} {x₀ : X'} {k : κ}
    (hk : EquicontinuousWithinAt (tX := t k) F S x₀) : EquicontinuousWithinAt (tX := ⨅ k, t k) F S x₀ :=
  by
  simp only [equicontinuousWithinAt_iff_continuousWithinAt (tX := _)] at hk ⊢
  unfold ContinuousWithinAt nhdsWithin at hk ⊢
  rw [nhds_iInf]
  exact hk.mono_left <| inf_le_inf_right _ <| iInf_le _ k

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