continuousOn_isOpen_of_generateFrom

English

If a family of opens h(t) holds for all t in T, then ContinuousOn f s holds for the topology generateFrom T.

Русский

Если для каждого t∈T открыто, то ContinuousOn f s верна для generateFrom T.

LaTeX

$$$(\\forall t \\in T, IsOpen (s \\cap f^{-1}(t))) \\Rightarrow ContinuousOn f s$$$

Lean4

theorem continuousOn_isOpen_of_generateFrom {β : Type*} {s : Set α} {T : Set (Set β)} {f : α → β}
    (h : ∀ t ∈ T, IsOpen (s ∩ f ⁻¹' t)) : @ContinuousOn α β _ (.generateFrom T) f s :=
  continuousOn_to_generateFrom_iff.2 fun _x hx t ht hxt => mem_nhdsWithin.2 ⟨_, h t ht, ⟨hx, hxt⟩, fun _y hy => hy.1.2⟩

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