α : Type u_1
β : Type ?u.5122
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
h : GenerateOpen {t | ∃ a, Ici aᶜ = t} s
⊢ IsLowerSet s
α : Type u_1
β : Type ?u.5122
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
h : IsOpen s
⊢ IsLowerSet s
replace h := isOpen_iff_generate_Ici_compl.1 h
case basic
α : Type u_1
β : Type ?u.5122
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s s✝ : Set α
a✝ : s✝ ∈ {t | ∃ a, Ici aᶜ = t}
⊢ IsLowerSet s✝

case univ
α : Type u_1
β : Type ?u.5122
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
⊢ IsLowerSet univ

case inter
α : Type u_1
β : Type ?u.5122
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s s✝ t✝ : Set α
a✝¹ : GenerateOpen {t | ∃ a, Ici aᶜ = t} s✝
a✝ : GenerateOpen {t | ∃ a, Ici aᶜ = t} t✝
a_ih✝¹ : IsLowerSet s✝
a_ih✝ : IsLowerSet t✝
⊢ IsLowerSet (s✝ ∩ t✝)

case sUnion
α : Type u_1
β : Type ?u.5122
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen {t | ∃ a, Ici aᶜ = t} s
a_ih✝ : ∀ (s : Set α), s ∈ S✝ → IsLowerSet s
⊢ IsLowerSet (⋃₀ S✝)
α : Type u_1
β : Type ?u.5122
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
h : GenerateOpen {t | ∃ a, Ici aᶜ = t} s
⊢ IsLowerSet s
induction h
case univ
α : Type u_1
β : Type ?u.5122
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
⊢ IsLowerSet univ

case inter
α : Type u_1
β : Type ?u.5122
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s s✝ t✝ : Set α
a✝¹ : GenerateOpen {t | ∃ a, Ici aᶜ = t} s✝
a✝ : GenerateOpen {t | ∃ a, Ici aᶜ = t} t✝
a_ih✝¹ : IsLowerSet s✝
a_ih✝ : IsLowerSet t✝
⊢ IsLowerSet (s✝ ∩ t✝)

case sUnion
α : Type u_1
β : Type ?u.5122
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen {t | ∃ a, Ici aᶜ = t} s
a_ih✝ : ∀ (s : Set α), s ∈ S✝ → IsLowerSet s
⊢ IsLowerSet (⋃₀ S✝)
case basic
α : Type u_1
β : Type ?u.5122
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s s✝ : Set α
a✝ : s✝ ∈ {t | ∃ a, Ici aᶜ = t}
⊢ IsLowerSet s✝

case univ
α : Type u_1
β : Type ?u.5122
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
⊢ IsLowerSet univ

case inter
α : Type u_1
β : Type ?u.5122
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s s✝ t✝ : Set α
a✝¹ : GenerateOpen {t | ∃ a, Ici aᶜ = t} s✝
a✝ : GenerateOpen {t | ∃ a, Ici aᶜ = t} t✝
a_ih✝¹ : IsLowerSet s✝
a_ih✝ : IsLowerSet t✝
⊢ IsLowerSet (s✝ ∩ t✝)

case sUnion
α : Type u_1
β : Type ?u.5122
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen {t | ∃ a, Ici aᶜ = t} s
a_ih✝ : ∀ (s : Set α), s ∈ S✝ → IsLowerSet s
⊢ IsLowerSet (⋃₀ S✝)
case basic u h' => obtain ⟨a, rfl⟩ := h'; exact (isUpperSet_Ici a).compl
case inter
α : Type u_1
β : Type ?u.5122
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s s✝ t✝ : Set α
a✝¹ : GenerateOpen {t | ∃ a, Ici aᶜ = t} s✝
a✝ : GenerateOpen {t | ∃ a, Ici aᶜ = t} t✝
a_ih✝¹ : IsLowerSet s✝
a_ih✝ : IsLowerSet t✝
⊢ IsLowerSet (s✝ ∩ t✝)

case sUnion
α : Type u_1
β : Type ?u.5122
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen {t | ∃ a, Ici aᶜ = t} s
a_ih✝ : ∀ (s : Set α), s ∈ S✝ → IsLowerSet s
⊢ IsLowerSet (⋃₀ S✝)
case univ
α : Type u_1
β : Type ?u.5122
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
⊢ IsLowerSet univ

case inter
α : Type u_1
β : Type ?u.5122
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s s✝ t✝ : Set α
a✝¹ : GenerateOpen {t | ∃ a, Ici aᶜ = t} s✝
a✝ : GenerateOpen {t | ∃ a, Ici aᶜ = t} t✝
a_ih✝¹ : IsLowerSet s✝
a_ih✝ : IsLowerSet t✝
⊢ IsLowerSet (s✝ ∩ t✝)

case sUnion
α : Type u_1
β : Type ?u.5122
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen {t | ∃ a, Ici aᶜ = t} s
a_ih✝ : ∀ (s : Set α), s ∈ S✝ → IsLowerSet s
⊢ IsLowerSet (⋃₀ S✝)
case univ => exact isLowerSet_univ
case sUnion
α : Type u_1
β : Type ?u.5122
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen {t | ∃ a, Ici aᶜ = t} s
a_ih✝ : ∀ (s : Set α), s ∈ S✝ → IsLowerSet s
⊢ IsLowerSet (⋃₀ S✝)
case inter
α : Type u_1
β : Type ?u.5122
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s s✝ t✝ : Set α
a✝¹ : GenerateOpen {t | ∃ a, Ici aᶜ = t} s✝
a✝ : GenerateOpen {t | ∃ a, Ici aᶜ = t} t✝
a_ih✝¹ : IsLowerSet s✝
a_ih✝ : IsLowerSet t✝
⊢ IsLowerSet (s✝ ∩ t✝)

case sUnion
α : Type u_1
β : Type ?u.5122
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen {t | ∃ a, Ici aᶜ = t} s
a_ih✝ : ∀ (s : Set α), s ∈ S✝ → IsLowerSet s
⊢ IsLowerSet (⋃₀ S✝)
case inter u v _ _ hu2 hv2 => exact hu2.inter hv2
no goals
case sUnion
α : Type u_1
β : Type ?u.5122
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen {t | ∃ a, Ici aᶜ = t} s
a_ih✝ : ∀ (s : Set α), s ∈ S✝ → IsLowerSet s
⊢ IsLowerSet (⋃₀ S✝)
case sUnion _ _ ih => exact isLowerSet_sUnion ih
case intro
α : Type u_1
β : Type ?u.5122
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
a : α
⊢ IsLowerSet (Ici aᶜ)
α : Type u_1
β : Type ?u.5122
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s u : Set α
h' : u ∈ {t | ∃ a, Ici aᶜ = t}
⊢ IsLowerSet u
obtain ⟨a, rfl⟩ := h'
no goals
case intro
α : Type u_1
β : Type ?u.5122
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
a : α
⊢ IsLowerSet (Ici aᶜ)
exact (isUpperSet_Ici a).compl
no goals
α : Type u_1
β : Type ?u.5122
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
⊢ IsLowerSet univ
exact isLowerSet_univ
no goals
α : Type u_1
β : Type ?u.5122
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s u v : Set α
a✝¹ : GenerateOpen {t | ∃ a, Ici aᶜ = t} u
a✝ : GenerateOpen {t | ∃ a, Ici aᶜ = t} v
hu2 : IsLowerSet u
hv2 : IsLowerSet v
⊢ IsLowerSet (u ∩ v)
exact hu2.inter hv2
no goals
α : Type u_1
β : Type ?u.5122
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen {t | ∃ a, Ici aᶜ = t} s
ih : ∀ (s : Set α), s ∈ S✝ → IsLowerSet s
⊢ IsLowerSet (⋃₀ S✝)
exact isLowerSet_sUnion ih