α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set (Set α)
hs : Set.Finite s
x✝ : ∀ (t : Set α), t ∈ ∅ → IsOpen t
⊢ IsOpen univ
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set (Set α)
hs : Set.Finite s
x✝ : ∀ (t : Set α), t ∈ ∅ → IsOpen t
⊢ IsOpen (⋂₀ ∅)
rw [sInter_empty]
no goals
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set (Set α)
hs : Set.Finite s
x✝ : ∀ (t : Set α), t ∈ ∅ → IsOpen t
⊢ IsOpen univ
exact isOpen_univ
α : Type u
β : Type v
ι : Sort w
a : α
s✝¹ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set (Set α)
hs : Set.Finite s
a✝ : Set α
s✝ : Set (Set α)
x✝¹ : ¬a✝ ∈ s✝
x✝ : Set.Finite s✝
ih : (∀ (t : Set α), t ∈ s✝ → IsOpen t) → IsOpen (⋂₀ s✝)
h : IsOpen a✝ ∧ ∀ (x : Set α), x ∈ s✝ → IsOpen x
⊢ IsOpen (a✝ ∩ ⋂₀ s✝)
α : Type u
β : Type v
ι : Sort w
a : α
s✝¹ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set (Set α)
hs : Set.Finite s
a✝ : Set α
s✝ : Set (Set α)
x✝¹ : ¬a✝ ∈ s✝
x✝ : Set.Finite s✝
ih : (∀ (t : Set α), t ∈ s✝ → IsOpen t) → IsOpen (⋂₀ s✝)
h : ∀ (t : Set α), t ∈ insert a✝ s✝ → IsOpen t
⊢ IsOpen (⋂₀ insert a✝ s✝)
simp only [sInter_insert, ball_insert_iff] at h ⊢
no goals
α : Type u
β : Type v
ι : Sort w
a : α
s✝¹ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set (Set α)
hs : Set.Finite s
a✝ : Set α
s✝ : Set (Set α)
x✝¹ : ¬a✝ ∈ s✝
x✝ : Set.Finite s✝
ih : (∀ (t : Set α), t ∈ s✝ → IsOpen t) → IsOpen (⋂₀ s✝)
h : IsOpen a✝ ∧ ∀ (x : Set α), x ∈ s✝ → IsOpen x
⊢ IsOpen (a✝ ∩ ⋂₀ s✝)
exact h.1.inter (ih h.2)