biSup_le_eq_sup — Mathlib

English

In a complete lattice, for any index i and function f, the supremum up to i satisfies ⨆_{j ≤ i} f(j) = (⨆_{j < i} f(j)) ⊔ f(i).

Русский

В полной решётке для любого индекса i и функции f выполняется: sup_{j≤i} f(j) = sup_{j<i} f(j) ⊔ f(i).

LaTeX

$$$$ \bigvee_{j \le i} f(j) = \bigvee_{j

Lean4

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

  simp only [le_refl, iSup_pos, iSup_and', lt_iff_le_and_ne, and_comm, sup_comm]

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