α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
⊢ 𝓝 a = ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s
α : Type u
g : Set (Set α)
a : α
⊢ 𝓝 a = ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s
letI := generateFrom g
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ IsOpen s}), 𝓟 s) = ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
⊢ 𝓝 a = ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s
rw [nhds_def]
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ IsOpen s}), 𝓟 s
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ IsOpen s}), 𝓟 s) = ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s
refine le_antisymm (biInf_mono fun s ⟨as, sg⟩ => ⟨as, .basic _ sg⟩) ?_
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
x✝ : s ∈ {s | a ∈ s ∧ IsOpen s}
ha : a ∈ s
hs : IsOpen s
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 s
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ IsOpen s}), 𝓟 s
refine le_iInf₂ fun s ⟨ha, hs⟩ => ?_
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
ha : a ∈ s
hs : IsOpen s
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 s
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
x✝ : s ∈ {s | a ∈ s ∧ IsOpen s}
ha : a ∈ s
hs : IsOpen s
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 s
clear ‹s ∈ { s | a ∈ s ∧ IsOpen s }›
case basic
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s s✝ : Set α
a✝ : s✝ ∈ g
ha : a ∈ s✝
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 s✝

case univ
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
ha : a ∈ univ
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 univ

case inter
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s s✝ t✝ : Set α
a✝¹ : GenerateOpen g s✝
a✝ : GenerateOpen g t✝
a_ih✝¹ : a ∈ s✝ → (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 s✝
a_ih✝ : a ∈ t✝ → (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 t✝
ha : a ∈ s✝ ∩ t✝
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 (s✝ ∩ t✝)

case sUnion
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen g s
a_ih✝ : ∀ (s : Set α), s ∈ S✝ → a ∈ s → (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 s
ha : a ∈ ⋃₀ S✝
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 (⋃₀ S✝)
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
ha : a ∈ s
hs : IsOpen s
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 s
induction hs
case univ
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
ha : a ∈ univ
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 univ

case inter
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s s✝ t✝ : Set α
a✝¹ : GenerateOpen g s✝
a✝ : GenerateOpen g t✝
a_ih✝¹ : a ∈ s✝ → (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 s✝
a_ih✝ : a ∈ t✝ → (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 t✝
ha : a ∈ s✝ ∩ t✝
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 (s✝ ∩ t✝)

case sUnion
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen g s
a_ih✝ : ∀ (s : Set α), s ∈ S✝ → a ∈ s → (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 s
ha : a ∈ ⋃₀ S✝
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 (⋃₀ S✝)
case basic
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s s✝ : Set α
a✝ : s✝ ∈ g
ha : a ∈ s✝
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 s✝

case univ
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
ha : a ∈ univ
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 univ

case inter
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s s✝ t✝ : Set α
a✝¹ : GenerateOpen g s✝
a✝ : GenerateOpen g t✝
a_ih✝¹ : a ∈ s✝ → (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 s✝
a_ih✝ : a ∈ t✝ → (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 t✝
ha : a ∈ s✝ ∩ t✝
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 (s✝ ∩ t✝)

case sUnion
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen g s
a_ih✝ : ∀ (s : Set α), s ∈ S✝ → a ∈ s → (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 s
ha : a ∈ ⋃₀ S✝
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 (⋃₀ S✝)
case basic hs => exact iInf₂_le _ ⟨ha, hs⟩
case inter
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s s✝ t✝ : Set α
a✝¹ : GenerateOpen g s✝
a✝ : GenerateOpen g t✝
a_ih✝¹ : a ∈ s✝ → (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 s✝
a_ih✝ : a ∈ t✝ → (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 t✝
ha : a ∈ s✝ ∩ t✝
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 (s✝ ∩ t✝)

case sUnion
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen g s
a_ih✝ : ∀ (s : Set α), s ∈ S✝ → a ∈ s → (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 s
ha : a ∈ ⋃₀ S✝
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 (⋃₀ S✝)
case univ
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
ha : a ∈ univ
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 univ

case inter
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s s✝ t✝ : Set α
a✝¹ : GenerateOpen g s✝
a✝ : GenerateOpen g t✝
a_ih✝¹ : a ∈ s✝ → (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 s✝
a_ih✝ : a ∈ t✝ → (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 t✝
ha : a ∈ s✝ ∩ t✝
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 (s✝ ∩ t✝)

case sUnion
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen g s
a_ih✝ : ∀ (s : Set α), s ∈ S✝ → a ∈ s → (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 s
ha : a ∈ ⋃₀ S✝
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 (⋃₀ S✝)
case univ => exact le_top.trans_eq principal_univ.symm
case sUnion
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen g s
a_ih✝ : ∀ (s : Set α), s ∈ S✝ → a ∈ s → (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 s
ha : a ∈ ⋃₀ S✝
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 (⋃₀ S✝)
case inter
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s s✝ t✝ : Set α
a✝¹ : GenerateOpen g s✝
a✝ : GenerateOpen g t✝
a_ih✝¹ : a ∈ s✝ → (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 s✝
a_ih✝ : a ∈ t✝ → (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 t✝
ha : a ∈ s✝ ∩ t✝
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 (s✝ ∩ t✝)

case sUnion
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen g s
a_ih✝ : ∀ (s : Set α), s ∈ S✝ → a ∈ s → (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 s
ha : a ∈ ⋃₀ S✝
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 (⋃₀ S✝)
case inter hs ht => exact (le_inf (hs ha.1) (ht ha.2)).trans_eq inf_principal
no goals
case sUnion
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen g s
a_ih✝ : ∀ (s : Set α), s ∈ S✝ → a ∈ s → (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 s
ha : a ∈ ⋃₀ S✝
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 (⋃₀ S✝)
case sUnion _S hS =>
  let ⟨t, htS, hat⟩ := ha
  exact (hS t htS hat).trans (principal_mono.2 <| subset_sUnion_of_mem htS)
no goals
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s s✝ : Set α
hs : s✝ ∈ g
ha : a ∈ s✝
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 s✝
exact iInf₂_le _ ⟨ha, hs⟩
no goals
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
ha : a ∈ univ
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 univ
exact le_top.trans_eq principal_univ.symm
no goals
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s s✝ t✝ : Set α
a✝¹ : GenerateOpen g s✝
a✝ : GenerateOpen g t✝
hs : a ∈ s✝ → (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 s✝
ht : a ∈ t✝ → (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 t✝
ha : a ∈ s✝ ∩ t✝
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 (s✝ ∩ t✝)
exact (le_inf (hs ha.1) (ht ha.2)).trans_eq inf_principal
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
S✝ : Set (Set α)
_S : ∀ (s : Set α), s ∈ S✝ → GenerateOpen g s
hS : ∀ (s : Set α), s ∈ S✝ → a ∈ s → (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 s
ha : a ∈ ⋃₀ S✝
t : Set α
htS : t ∈ S✝
hat : a ∈ t
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 (⋃₀ S✝)
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
S✝ : Set (Set α)
_S : ∀ (s : Set α), s ∈ S✝ → GenerateOpen g s
hS : ∀ (s : Set α), s ∈ S✝ → a ∈ s → (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 s
ha : a ∈ ⋃₀ S✝
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 (⋃₀ S✝)
let ⟨t, htS, hat⟩ := ha
no goals
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
S✝ : Set (Set α)
_S : ∀ (s : Set α), s ∈ S✝ → GenerateOpen g s
hS : ∀ (s : Set α), s ∈ S✝ → a ∈ s → (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 s
ha : a ∈ ⋃₀ S✝
t : Set α
htS : t ∈ S✝
hat : a ∈ t
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ g}), 𝓟 s) ≤ 𝓟 (⋃₀ S✝)
exact (hS t htS hat).trans (principal_mono.2 <| subset_sUnion_of_mem htS)