biSup_sup — Mathlib

English

If there exists i with p i, then the supremum of i of a and f i h equals the supremum of i of f i h with a max.

Русский

Если существует i с p(i), то суперa ⊔ f(i) равен максимуму между a и f(i).

LaTeX

$$$ \\mathrm{max}\\left( a, \\bigvee_{i} f(i) \\right) = \\bigvee_{i} \\mathrm{max}( a, f(i) ). $$$

Lean4

theorem biSup_sup {p : ι → Prop} {f : ∀ i, p i → α} {a : α} (h : ∃ i, p i) :
    (⨆ (i) (h : p i), f i h) ⊔ a = ⨆ (i) (h : p i), f i h ⊔ a :=
  by
  haveI : Nonempty { i // p i } :=
    let ⟨i, hi⟩ := h
    ⟨⟨i, hi⟩⟩
  rw [iSup_subtype', iSup_subtype', iSup_sup]

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