iUnion_Iic_coe_nat — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem iUnion_Iic_coe_nat : ⋃ n : ℕ, Iic (n : ℝ≥0∞) = {∞}ᶜ :=
  Subset.antisymm (iUnion_subset fun n _x hx => ne_top_of_le_ne_top (natCast_ne_top n) hx) <|
    iUnion_Iio_coe_nat ▸ iUnion_mono fun _ => Iio_subset_Iic_self

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