iUnion_Iio_coe_nat

Mathlib.Data.ENNReal.Basic

URI: https://scilib.ai/kg/mathlib#ENNReal.iUnion_Iio_coe_nat

← MathLib Explorer

English

The union over all natural n of Iio(n) equals the complement of {∞}.

Русский

Объединение по всем натуральным n Iio(n) равно дополнению к {∞}.

LaTeX

$$$ \bigcup_{n \in \mathbb{N}} Iio(n) = {\\infty}^{c} $$$

Lean4

@[simp]
theorem iUnion_Iio_coe_nat : ⋃ n : ℕ, Iio (n : ℝ≥0∞) = {∞}ᶜ :=
  by
  ext x
  rw [mem_iUnion]
  exact ⟨fun ⟨n, hn⟩ => ne_top_of_lt hn, ENNReal.exists_nat_gt⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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