biUnion_Ico_eq_Iio_self_iff — Mathlib

English

For p i → Prop and f(i, hi) in α, the union over i and hi of Ico(f i hi, a) equals Iio(a) iff for all x < a there exists i and hi with f i hi ≤ x.

Русский

Для p и f(i, hi) в α объединение по i и hi интервалов Ico(f i hi, a) равно Iio(a) тогда и только тогда, когда для каждого x < a существует i и hi с f i hi ≤ x.

LaTeX

$$$$\bigcup_i\bigcup_{hi} Ico(f_i hi, a) = Iio(a) \iff \forall x

Lean4

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

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