α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ s ∈ (𝓝 a).sets ↔ ∃ t, t ∈ b ∧ a ∈ t ∧ t ⊆ s
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ s ∈ 𝓝 a ↔ ∃ t, t ∈ b ∧ a ∈ t ∧ t ⊆ s
change s ∈ (𝓝 a).sets ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ (s ∈ ⋃ (i : Set α) (_ : i ∈ {s | a ∈ s ∧ s ∈ b}), (𝓟 i).sets) ↔ ∃ t, t ∈ b ∧ a ∈ t ∧ t ⊆ s

case h
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ DirectedOn ((fun s => 𝓟 s) ⁻¹'o fun x x_1 => x ≥ x_1) {s | a ∈ s ∧ s ∈ b}

case ne
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ Set.Nonempty {s | a ∈ s ∧ s ∈ b}
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ s ∈ (𝓝 a).sets ↔ ∃ t, t ∈ b ∧ a ∈ t ∧ t ⊆ s
rw [hb.eq_generateFrom, nhds_generateFrom, biInf_sets_eq]
no goals
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ (s ∈ ⋃ (i : Set α) (_ : i ∈ {s | a ∈ s ∧ s ∈ b}), (𝓟 i).sets) ↔ ∃ t, t ∈ b ∧ a ∈ t ∧ t ⊆ s
simp [and_assoc, and_left_comm]
case h.intro.intro
α : Type u
t✝ : TopologicalSpace α
a : α
s✝ : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
s : Set α
hs₁ : a ∈ s
hs₂ : s ∈ b
t : Set α
ht₁ : a ∈ t
ht₂ : t ∈ b
⊢ ∃ z,
    z ∈ {s | a ∈ s ∧ s ∈ b} ∧
      ((fun s => 𝓟 s) ⁻¹'o fun x x_1 => x ≥ x_1) s z ∧ ((fun s => 𝓟 s) ⁻¹'o fun x x_1 => x ≥ x_1) t z
case h
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ DirectedOn ((fun s => 𝓟 s) ⁻¹'o fun x x_1 => x ≥ x_1) {s | a ∈ s ∧ s ∈ b}
rintro s ⟨hs₁, hs₂⟩ t ⟨ht₁, ht₂⟩
case h.intro.intro
α : Type u
t✝ : TopologicalSpace α
a : α
s✝ : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
s : Set α
hs₁ : a ∈ s
hs₂ : s ∈ b
t : Set α
ht₁ : a ∈ t
ht₂ : t ∈ b
u : Set α
hu₁ : u ∈ b
hu₂ : a ∈ u
hu₃ : u ⊆ s ∩ t
⊢ ∃ z,
    z ∈ {s | a ∈ s ∧ s ∈ b} ∧
      ((fun s => 𝓟 s) ⁻¹'o fun x x_1 => x ≥ x_1) s z ∧ ((fun s => 𝓟 s) ⁻¹'o fun x x_1 => x ≥ x_1) t z
case h.intro.intro
α : Type u
t✝ : TopologicalSpace α
a : α
s✝ : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
s : Set α
hs₁ : a ∈ s
hs₂ : s ∈ b
t : Set α
ht₁ : a ∈ t
ht₂ : t ∈ b
⊢ ∃ z,
    z ∈ {s | a ∈ s ∧ s ∈ b} ∧
      ((fun s => 𝓟 s) ⁻¹'o fun x x_1 => x ≥ x_1) s z ∧ ((fun s => 𝓟 s) ⁻¹'o fun x x_1 => x ≥ x_1) t z
let ⟨u, hu₁, hu₂, hu₃⟩ := hb.1 _ hs₂ _ ht₂ _ ⟨hs₁, ht₁⟩
no goals
case h.intro.intro
α : Type u
t✝ : TopologicalSpace α
a : α
s✝ : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
s : Set α
hs₁ : a ∈ s
hs₂ : s ∈ b
t : Set α
ht₁ : a ∈ t
ht₂ : t ∈ b
u : Set α
hu₁ : u ∈ b
hu₂ : a ∈ u
hu₃ : u ⊆ s ∩ t
⊢ ∃ z,
    z ∈ {s | a ∈ s ∧ s ∈ b} ∧
      ((fun s => 𝓟 s) ⁻¹'o fun x x_1 => x ≥ x_1) s z ∧ ((fun s => 𝓟 s) ⁻¹'o fun x x_1 => x ≥ x_1) t z
exact ⟨u, ⟨hu₂, hu₁⟩, le_principal_iff.2 (hu₃.trans (inter_subset_left _ _)),
  le_principal_iff.2 (hu₃.trans (inter_subset_right _ _))⟩
case ne.intro.intro
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
i : Set α
h1 : i ∈ b
h2 : a ∈ i
⊢ Set.Nonempty {s | a ∈ s ∧ s ∈ b}
case ne
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ Set.Nonempty {s | a ∈ s ∧ s ∈ b}
rcases eq_univ_iff_forall.1 hb.sUnion_eq a with ⟨i, h1, h2⟩
no goals
case ne.intro.intro
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
i : Set α
h1 : i ∈ b
h2 : a ∈ i
⊢ Set.Nonempty {s | a ∈ s ∧ s ∈ b}
exact ⟨i, h2, h1⟩