English
The lift of a supremum equals the supremum of the lifts.
Русский
Перенос верхней грани (lift) равен верхней грани перенесённого множества.
LaTeX
$$$\text{lift}\,(sSup\,s) = sSup(\text{lift} \;''\,s)$$$
Lean4
/-- The lift of a supremum is the supremum of the lifts. -/
theorem lift_sSup {s : Set Cardinal} (hs : BddAbove s) : lift.{u} (sSup s) = sSup (lift.{u} '' s) :=
by
apply ((le_csSup_iff' (bddAbove_image.{_, u} _ hs)).2 fun c hc => _).antisymm (csSup_le' _)
· intro c hc
by_contra h
obtain ⟨d, rfl⟩ := Cardinal.mem_range_lift_of_le (not_le.1 h).le
simp_rw [lift_le] at h hc
rw [csSup_le_iff' hs] at h
exact h fun a ha => lift_le.1 <| hc (mem_image_of_mem _ ha)
· rintro i ⟨j, hj, rfl⟩
exact lift_le.2 (le_csSup hs hj)
