α : Type u
inst✝ : OmegaCompletePartialOrder α
s : Set (Set α)
hs : ∀ (t : Set α), t ∈ s → Continuous' fun x => x ∈ t
⊢ Continuous' fun x => x ∈ ⋃₀ s
α : Type u
inst✝ : OmegaCompletePartialOrder α
s : Set (Set α)
hs : ∀ (t : Set α), t ∈ s → IsOpen α t
⊢ IsOpen α (⋃₀ s)
simp only [IsOpen] at hs⊢
case h.e'_5.h.a
α : Type u
inst✝ : OmegaCompletePartialOrder α
s : Set (Set α)
hs : ∀ (t : Set α), t ∈ s → Continuous' fun x => x ∈ t
x✝ : α
⊢ x✝ ∈ ⋃₀ s ↔ sSup (setOf ⁻¹' s) x✝
α : Type u
inst✝ : OmegaCompletePartialOrder α
s : Set (Set α)
hs : ∀ (t : Set α), t ∈ s → Continuous' fun x => x ∈ t
⊢ Continuous' fun x => x ∈ ⋃₀ s
convert CompleteLattice.sSup_continuous' (setOf ⁻¹' s) hs
no goals
case h.e'_5.h.a
α : Type u
inst✝ : OmegaCompletePartialOrder α
s : Set (Set α)
hs : ∀ (t : Set α), t ∈ s → Continuous' fun x => x ∈ t
x✝ : α
⊢ x✝ ∈ ⋃₀ s ↔ sSup (setOf ⁻¹' s) x✝
simp only [sSup_apply, setOf_bijective.surjective.exists, exists_prop, mem_preimage,
  SetCoe.exists, iSup_Prop_eq, mem_setOf_eq, mem_sUnion]