α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLattice α
inst✝⁴ : CompleteLattice β
inst✝³ : TopologicalSpace α
inst✝² : LowerTopology α
inst✝¹ : TopologicalSpace β
inst✝ : LowerTopology β
f : sInfHom α β
b : β
⊢ IsClosed (↑f ⁻¹' Ici b)
α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLattice α
inst✝⁴ : CompleteLattice β
inst✝³ : TopologicalSpace α
inst✝² : LowerTopology α
inst✝¹ : TopologicalSpace β
inst✝ : LowerTopology β
f : sInfHom α β
⊢ Continuous ↑f
refine LowerTopology.continuous_of_Ici fun b => ?_
case h.e'_3
α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLattice α
inst✝⁴ : CompleteLattice β
inst✝³ : TopologicalSpace α
inst✝² : LowerTopology α
inst✝¹ : TopologicalSpace β
inst✝ : LowerTopology β
f : sInfHom α β
b : β
⊢ ↑f ⁻¹' Ici b = Ici (sInf (↑f ⁻¹' Ici b))
α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLattice α
inst✝⁴ : CompleteLattice β
inst✝³ : TopologicalSpace α
inst✝² : LowerTopology α
inst✝¹ : TopologicalSpace β
inst✝ : LowerTopology β
f : sInfHom α β
b : β
⊢ IsClosed (↑f ⁻¹' Ici b)
convert LowerTopology.isClosed_Ici (sInf <| f ⁻¹' Ici b)
case h.e'_3
α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLattice α
inst✝⁴ : CompleteLattice β
inst✝³ : TopologicalSpace α
inst✝² : LowerTopology α
inst✝¹ : TopologicalSpace β
inst✝ : LowerTopology β
f : sInfHom α β
b : β
a : α
ha : a ∈ Ici (sInf (↑f ⁻¹' Ici b))
⊢ b ≤ ↑↑f (sInf (↑f ⁻¹' Ici b))
case h.e'_3
α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLattice α
inst✝⁴ : CompleteLattice β
inst✝³ : TopologicalSpace α
inst✝² : LowerTopology α
inst✝¹ : TopologicalSpace β
inst✝ : LowerTopology β
f : sInfHom α β
b : β
⊢ ↑f ⁻¹' Ici b = Ici (sInf (↑f ⁻¹' Ici b))
refine' Subset.antisymm (fun a => sInf_le) fun a ha => le_trans _ <|
  OrderHomClass.mono (f : α →o β) ha
case h.e'_3
α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLattice α
inst✝⁴ : CompleteLattice β
inst✝³ : TopologicalSpace α
inst✝² : LowerTopology α
inst✝¹ : TopologicalSpace β
inst✝ : LowerTopology β
f : sInfHom α β
b : β
a : α
ha : a ∈ Ici (sInf (↑f ⁻¹' Ici b))
⊢ b ≤ sInf (↑f '' (↑f ⁻¹' Ici b))
case h.e'_3
α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLattice α
inst✝⁴ : CompleteLattice β
inst✝³ : TopologicalSpace α
inst✝² : LowerTopology α
inst✝¹ : TopologicalSpace β
inst✝ : LowerTopology β
f : sInfHom α β
b : β
a : α
ha : a ∈ Ici (sInf (↑f ⁻¹' Ici b))
⊢ b ≤ ↑↑f (sInf (↑f ⁻¹' Ici b))
refine' LE.le.trans _ (map_sInf f _).ge
no goals
case h.e'_3
α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLattice α
inst✝⁴ : CompleteLattice β
inst✝³ : TopologicalSpace α
inst✝² : LowerTopology α
inst✝¹ : TopologicalSpace β
inst✝ : LowerTopology β
f : sInfHom α β
b : β
a : α
ha : a ∈ Ici (sInf (↑f ⁻¹' Ici b))
⊢ b ≤ sInf (↑f '' (↑f ⁻¹' Ici b))
simp