iUnion_Ioc_eq_Ioi_self_iff — Mathlib

English

For f: ι → α in a linear order, ⋃ Ioc(a, f i) equals Ioi(a) iff for all x > a there exists i with x ≤ f i.

Русский

Для f: ι → α в линейном порядке, ⋃ Ioc(a, f i) = Ioi(a) эквивалентно тому, что для каждого x > a найдется i с x ≤ f i.

LaTeX

$$$$ \bigcup_i Ioc(a, f_i) = Ioi(a) \iff \forall x>a, \exists i, x \le f_i $$$$

Lean4

@[simp]
theorem iUnion_Ioc_eq_Ioi_self_iff {f : ι → α} {a : α} : ⋃ i, Ioc a (f i) = Ioi a ↔ ∀ x, a < x → ∃ i, x ≤ f i := by
  simp [← Ioi_inter_Iic, ← inter_iUnion, subset_def]

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