English
If not all i satisfy p i, then the bi-supremum over i and h of f(⟨i,h⟩) equals iSup f ⊔ sSup ∅.
Русский
Если не все i удовлетворяют p i, то надсупремум по i и h f(⟨i,h⟩) равен iSup f ⊔ sSup ∅.
LaTeX
$$$\text{If } \lnot(\forall i, p(i)):\sup_{i} \sup_{h: p(i)} f(\langle i,h\rangle) = iSup f \; \sqcup \; sSup\emptyset.$$$
Lean4
theorem cbiSup_eq_of_not_forall {p : ι → Prop} {f : Subtype p → α} (hp : ¬(∀ i, p i)) :
⨆ (i) (h : p i), f ⟨i, h⟩ = iSup f ⊔ sSup ∅ := by
classical
rcases not_forall.1 hp with ⟨i₀, hi₀⟩
have : Nonempty ι := ⟨i₀⟩
simp only [ciSup_eq_ite]
by_cases H : BddAbove (range f)
· have B : BddAbove (range fun i ↦ if h : p i then f ⟨i, h⟩ else sSup ∅) :=
by
rcases H with ⟨c, hc⟩
refine ⟨c ⊔ sSup ∅, ?_⟩
rintro - ⟨i, rfl⟩
by_cases hi : p i
· simp only [hi, dite_true, le_sup_iff, hc (mem_range_self _), true_or]
· simp only [hi, dite_false, le_sup_right]
apply le_antisymm
· apply ciSup_le (fun i ↦ ?_)
by_cases hi : p i
· simp only [hi, dite_true, le_sup_iff]
left
exact le_ciSup H _
· simp [hi]
· apply sup_le
· rcases isEmpty_or_nonempty (Subtype p) with hp | hp
· rw [iSup_of_empty']
convert le_ciSup B i₀
simp [hi₀]
· apply ciSup_le
rintro ⟨i, hi⟩
convert le_ciSup B i
simp [hi]
· convert le_ciSup B i₀
simp [hi₀]
· have : iSup f = sSup (∅ : Set α) := csSup_of_not_bddAbove H
simp only [this, le_refl, sup_of_le_left]
apply csSup_of_not_bddAbove
contrapose! H
apply H.mono
rintro - ⟨i, rfl⟩
convert mem_range_self i.1
simp [i.2]
