English
For a family f(i, j) with i in index ι and j in index ι', the double supremum equals the top element if and only if for every b < ⊤ there exist i, j with b < f(i, j).
Русский
Для семейства f(i, j) существует двойной верхний предел, равный ⊤, тогда и только если для каждого b < ⊤ найдутся i, j такие, что b < f(i, j).
LaTeX
$$$\\displaystyle (\\big\\vee_{i} \\big\\vee_{j} f(i,j)) = \\top \\iff \\forall b < \\top, \\exists i \\exists j, b < f(i,j)$$$
Lean4
/-- When taking the supremum of `f : ι → α`, the elements of `ι` on which `f` gives `⊥` can be
dropped, without changing the result. -/
@[simp]
theorem iSup_ne_bot_subtype (f : ι → α) : ⨆ i : { i // f i ≠ ⊥ }, f i = ⨆ i, f i :=
by
by_cases htriv : ∀ i, f i = ⊥
· simp only [iSup_bot, (funext htriv : f = _)]
refine (iSup_comp_le f _).antisymm (iSup_mono' fun i => ?_)
by_cases hi : f i = ⊥
· rw [hi]
obtain ⟨i₀, hi₀⟩ := not_forall.mp htriv
exact ⟨⟨i₀, hi₀⟩, bot_le⟩
· exact ⟨⟨i, hi⟩, rfl.le⟩
