continuousAt — Mathlib

English

If IsEvenlyCovered f (f x) I, then f is continuous at x.

Русский

Если x равномерно покрыт f через волокно I, то f непрерывна в x.

LaTeX

$$$\\text{ContinuousAt}(f, x)$$$

Lean4

protected theorem continuousAt {x : E} (h : IsEvenlyCovered f (f x) I) : ContinuousAt f x :=
  have ⟨_, _, hxU, _, _, H, _⟩ := h
  have : Nonempty I := ⟨(H ⟨x, hxU⟩).2⟩
  let e := h.toTrivialization
  e.continuousAt_proj (e.mem_source.mpr (mem_toTrivialization_baseSet h))

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