Iio_mem_nhds

Mathlib.Topology.Algebra.WithZeroTopology

URI: https://scilib.ai/kg/mathlib#WithZeroTopology.Iio_mem_nhds

English

If γ₁ < γ₂, then Iio(γ₂) is a neighborhood of γ₁ in this topology.

Русский

Если γ₁ < γ₂, то Iio(γ₂) является окрестностью γ₁ в этой топологии.

LaTeX

$$$Iio(γ_2) \in \mathcal{N}(γ_1) \quad (γ_1 < γ_2)$$$

Lean4

theorem Iio_mem_nhds (h : γ₁ < γ₂) : Iio γ₂ ∈ 𝓝 γ₁ := by
  rcases eq_or_ne γ₁ 0 with (rfl | h₀) <;> simp [*, h.ne', Iio_mem_nhds_zero]

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

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

Разделы

Аффилиация

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