English
If f is a normal function between ConditionallyCompleteLinearOrders, and the preimage of Iic x is nonempty and bounded above, then it equals Iic (sSup (preimage f (Iic x))).
Русский
Пусть f — нормальная функция между ConditionallyCompleteLinearOrder. Тогда f^{-1}(Iic(x)) непусто и ограничено сверху тогда, когда оно равно Iic( sSup( f^{-1}(Iic(x)) ) ).
LaTeX
$$$\\mathrm{IsNormal}(f) \\Rightarrow \\forall x,\\ (f^{-1}'Iic x).\\Nonempty \\wedge BddAbove(f^{-1}'Iic x) \\Rightarrow f^{-1}'Iic x = Iic( sSup( f^{-1}'Iic x )).$$$
Lean4
theorem preimage_Iic (hf : IsNormal f) {x : β} (h₁ : (f ⁻¹' Iic x).Nonempty) (h₂ : BddAbove (f ⁻¹' Iic x)) :
f ⁻¹' Iic x = Iic (sSup (f ⁻¹' Iic x)) :=
by
refine le_antisymm (fun _ ↦ le_csSup h₂) (fun y hy ↦ ?_)
obtain hy | rfl := hy.lt_or_eq
· rw [lt_csSup_iff h₂ h₁] at hy
obtain ⟨z, hz, hyz⟩ := hy
exact (hf.strictMono hyz).le.trans hz
· rw [mem_preimage, hf.map_sSup h₁ h₂]
apply (csSup_le_csSup bddAbove_Iic _ (image_preimage_subset ..)).trans
· rw [csSup_Iic]
· simpa
