limUnder_eq

Mathlib.Topology.Separation.Hausdorff

URI: https://scilib.ai/kg/mathlib#Filter.Tendsto.limUnder_eq

English

A singleton is a Gδ set in a space with FirstCountable topology and T1 separation.

Русский

Одиночка является множеством Gδ в пространстве с первой счетностью и T1-разделением.

LaTeX

$$$\\text{singleton} \\in \\mathrm{IsGδ}$$$

Lean4

theorem limUnder_eq {x : X} {f : Filter Y} [NeBot f] {g : Y → X} (h : Tendsto g f (𝓝 x)) :
    @limUnder _ _ _ ⟨x⟩ f g = x :=
  lim_eq h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru