biSup_ge_eq_sup — Mathlib

English

For any index i in a complete lattice, the supremum over j ≥ i equals f(i) joined with the supremum over j > i: ⨆_{j ≥ i} f(j) = f(i) ⊔ (⨆_{j>i} f(j)).

Русский

Для любого i в полной решётке верхняя граница по j ≥ i равна объединению f(i) и верхней границы по j>i: ⨆_{j ≥ i} f(j) = f(i) ⊔ (⨆_{j>i} f(j)).

LaTeX

$$$$ \bigvee_{j \ge i} f(j) = f(i) \vee \bigvee_{j > i} f(j) $$$$

Lean4

theorem biSup_ge_eq_sup : (⨆ j ≥ i, f j) = f i ⊔ (⨆ j > i, f j) :=
  by
  rw [iSup_split_single _ i]
    -- Squeezed for a ~10x speedup, though it's still reasonably fast unsqueezed.

  simp only [ge_iff_le, le_refl, iSup_pos, ne_comm, iSup_and', gt_iff_lt, lt_iff_le_and_ne, and_comm]

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