iSup_extend_bot — Mathlib

English

Again, for an injective e: ι → β and f: ι → α, the supremum over j of extend e f at ⊥ equals the supremum over i of f i.

Русский

Повторяется тот же факт для инъективного e: ⨆ j, extend e f ⊥ j = ⨆ i, f i.

LaTeX

$$$$ \\bigvee_{j} (\\mathrm{extend}\\,e\\,f\\,\\bot)(j) = \\bigvee_{i} f(i) $$$$

Lean4

theorem iSup_extend_bot {e : ι → β} (he : Injective e) (f : ι → α) : ⨆ j, extend e f ⊥ j = ⨆ i, f i :=
  by
  rw [iSup_split _ fun j => ∃ i, e i = j]
  simp +contextual [he.extend_apply, extend_apply', @iSup_comm _ β ι]

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