biUnion_Ioc_eq_Ioi_self_iff — Mathlib

English

Similarly to the previous, but with Ioc(a, f i hi) and Ioi(a): the union over i and hi of Ioc a (f i hi) equals Ioi(a) iff for all x > a there exists i with x ≤ f i hi.

Русский

Аналогично предыдущему, но с Ioc(a, f i hi) против Ioi(a): объединение по i и hi интервалов Ioc a (f i hi) даёт Ioi(a) тогда и только тогда, когда для каждого x > a существует i с x ≤ f i hi.

LaTeX

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

Lean4

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

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