iUnion_Ico_eq_Iio_self_iff — Mathlib

English

For f: ι → α in a linear order, the equivalence between ⋃ Ico(f i) a and Iio a holds iff for every x < a there exists i with f(i) ≤ x.

Русский

Для отображения f: ι → α в линейном порядке равносильность ⋃ Ico(f(i), a) = Iio(a) равна тому, что для любого x < a существует i с f(i) ≤ x.

LaTeX

$$$$\bigcup_i Ico(f_i,a) = Iio(a) \iff \forall x < a, \exists i, f_i \le x $$$$

Lean4

@[simp]
theorem iUnion_Ico_eq_Iio_self_iff {f : ι → α} {a : α} : ⋃ i, Ico (f i) a = Iio a ↔ ∀ x < a, ∃ i, f i ≤ x := by
  simp [← Ici_inter_Iio, ← iUnion_inter, subset_def]

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