case tfae_1_iff_5
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
⊢ RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a

α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
⊢ List.TFAE
    [RegularSpace X, ∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a),
      ∀ (a : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 a) ↔ ¬a ∈ closure s,
      ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s, ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a,
      ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a]
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
⊢ List.TFAE
    [RegularSpace X, ∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a),
      ∀ (a : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 a) ↔ ¬a ∈ closure s,
      ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s, ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a,
      ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a]
tfae_have 1 ↔ 5
case tfae_5_to_6
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
⊢ (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a

α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
⊢ List.TFAE
    [RegularSpace X, ∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a),
      ∀ (a : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 a) ↔ ¬a ∈ closure s,
      ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s, ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a,
      ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a]
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
⊢ List.TFAE
    [RegularSpace X, ∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a),
      ∀ (a : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 a) ↔ ¬a ∈ closure s,
      ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s, ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a,
      ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a]
tfae_have 5 → 6
case tfae_6_to_4
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
⊢ (∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a) → ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s

α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
tfae_6_to_4 :
  (∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a) → ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
⊢ List.TFAE
    [RegularSpace X, ∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a),
      ∀ (a : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 a) ↔ ¬a ∈ closure s,
      ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s, ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a,
      ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a]
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
⊢ List.TFAE
    [RegularSpace X, ∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a),
      ∀ (a : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 a) ↔ ¬a ∈ closure s,
      ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s, ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a,
      ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a]
tfae_have 6 → 4
case tfae_4_to_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
tfae_6_to_4 :
  (∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a) → ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
⊢ (∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s) →
    ∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a)

α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
tfae_6_to_4 :
  (∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a) → ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
tfae_4_to_2 :
  (∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s) →
    ∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a)
⊢ List.TFAE
    [RegularSpace X, ∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a),
      ∀ (a : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 a) ↔ ¬a ∈ closure s,
      ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s, ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a,
      ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a]
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
tfae_6_to_4 :
  (∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a) → ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
⊢ List.TFAE
    [RegularSpace X, ∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a),
      ∀ (a : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 a) ↔ ¬a ∈ closure s,
      ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s, ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a,
      ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a]
tfae_have 4 → 2
case tfae_2_to_3
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
tfae_6_to_4 :
  (∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a) → ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
tfae_4_to_2 :
  (∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s) →
    ∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a)
⊢ (∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a)) →
    ∀ (a : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 a) ↔ ¬a ∈ closure s

α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
tfae_6_to_4 :
  (∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a) → ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
tfae_4_to_2 :
  (∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s) →
    ∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a)
tfae_2_to_3 :
  (∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a)) →
    ∀ (a : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 a) ↔ ¬a ∈ closure s
⊢ List.TFAE
    [RegularSpace X, ∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a),
      ∀ (a : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 a) ↔ ¬a ∈ closure s,
      ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s, ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a,
      ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a]
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
tfae_6_to_4 :
  (∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a) → ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
tfae_4_to_2 :
  (∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s) →
    ∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a)
⊢ List.TFAE
    [RegularSpace X, ∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a),
      ∀ (a : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 a) ↔ ¬a ∈ closure s,
      ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s, ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a,
      ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a]
tfae_have 2 → 3
case tfae_3_to_1
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
tfae_6_to_4 :
  (∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a) → ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
tfae_4_to_2 :
  (∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s) →
    ∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a)
tfae_2_to_3 :
  (∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a)) →
    ∀ (a : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 a) ↔ ¬a ∈ closure s
⊢ (∀ (a : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 a) ↔ ¬a ∈ closure s) → RegularSpace X

α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
tfae_6_to_4 :
  (∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a) → ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
tfae_4_to_2 :
  (∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s) →
    ∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a)
tfae_2_to_3 :
  (∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a)) →
    ∀ (a : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 a) ↔ ¬a ∈ closure s
tfae_3_to_1 : (∀ (a : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 a) ↔ ¬a ∈ closure s) → RegularSpace X
⊢ List.TFAE
    [RegularSpace X, ∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a),
      ∀ (a : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 a) ↔ ¬a ∈ closure s,
      ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s, ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a,
      ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a]
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
tfae_6_to_4 :
  (∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a) → ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
tfae_4_to_2 :
  (∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s) →
    ∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a)
tfae_2_to_3 :
  (∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a)) →
    ∀ (a : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 a) ↔ ¬a ∈ closure s
⊢ List.TFAE
    [RegularSpace X, ∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a),
      ∀ (a : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 a) ↔ ¬a ∈ closure s,
      ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s, ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a,
      ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a]
tfae_have 3 → 1
no goals
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
tfae_6_to_4 :
  (∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a) → ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
tfae_4_to_2 :
  (∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s) →
    ∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a)
tfae_2_to_3 :
  (∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a)) →
    ∀ (a : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 a) ↔ ¬a ∈ closure s
tfae_3_to_1 : (∀ (a : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 a) ↔ ¬a ∈ closure s) → RegularSpace X
⊢ List.TFAE
    [RegularSpace X, ∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a),
      ∀ (a : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 a) ↔ ¬a ∈ closure s,
      ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s, ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a,
      ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a]
tfae_finish
case tfae_1_iff_5
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
⊢ (∀ (y : X) (x : Set X), IsClosed (xᶜ) → ¬y ∈ xᶜ → Disjoint (𝓝ˢ (xᶜ)) (𝓝 y)) ↔
    ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
case tfae_1_iff_5
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
⊢ RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
rw [regularSpace_iff, (@compl_surjective (Set X) _).forall, forall_swap]
no goals
case tfae_1_iff_5
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
⊢ (∀ (y : X) (x : Set X), IsClosed (xᶜ) → ¬y ∈ xᶜ → Disjoint (𝓝ˢ (xᶜ)) (𝓝 y)) ↔
    ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
simp only [isClosed_compl_iff, mem_compl_iff, Classical.not_not, @and_comm (_ ∈ _),
  (nhds_basis_opens _).lift'_closure.le_basis_iff (nhds_basis_opens _), and_imp,
  (nhds_basis_opens _).disjoint_iff_right, exists_prop, ← subset_interior_iff_mem_nhdsSet,
  interior_compl, compl_subset_compl]
no goals
case tfae_5_to_6
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
⊢ (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
exact fun h a => (h a).antisymm (𝓝 _).le_lift'_closure
case tfae_6_to_4
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
H : ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
a : X
s : Set X
hs : s ∈ 𝓝 a
⊢ ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
case tfae_6_to_4
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
⊢ (∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a) → ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
intro H a s hs
case tfae_6_to_4
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
H : ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
a : X
s : Set X
hs : s ∈ Filter.lift' (𝓝 a) closure
⊢ ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
case tfae_6_to_4
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
H : ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
a : X
s : Set X
hs : s ∈ 𝓝 a
⊢ ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
rw [← H] at hs
case tfae_6_to_4.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
H : ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
a : X
s : Set X
hs : s ∈ Filter.lift' (𝓝 a) closure
U : Set X
hU : U ∈ 𝓝 a
hUs : closure (id U) ⊆ s
⊢ ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
case tfae_6_to_4
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
H : ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
a : X
s : Set X
hs : s ∈ Filter.lift' (𝓝 a) closure
⊢ ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
rcases(𝓝 a).basis_sets.lift'_closure.mem_iff.mp hs with ⟨U, hU, hUs⟩
no goals
case tfae_6_to_4.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
H : ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
a : X
s : Set X
hs : s ∈ Filter.lift' (𝓝 a) closure
U : Set X
hU : U ∈ 𝓝 a
hUs : closure (id U) ⊆ s
⊢ ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
exact ⟨closure U, mem_of_superset hU subset_closure, isClosed_closure, hUs⟩
case tfae_4_to_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
tfae_6_to_4 :
  (∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a) → ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
H : ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
s : Set X
a : X
ha : ¬a ∈ closure s
⊢ Disjoint (𝓝ˢ s) (𝓝 a)
case tfae_4_to_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
tfae_6_to_4 :
  (∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a) → ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
⊢ (∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s) →
    ∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a)
intro H s a ha
case tfae_4_to_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
tfae_6_to_4 :
  (∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a) → ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
H : ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
s : Set X
a : X
ha : ¬a ∈ closure s
ha' : sᶜ ∈ 𝓝 a
⊢ Disjoint (𝓝ˢ s) (𝓝 a)
case tfae_4_to_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
tfae_6_to_4 :
  (∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a) → ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
H : ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
s : Set X
a : X
ha : ¬a ∈ closure s
⊢ Disjoint (𝓝ˢ s) (𝓝 a)
have ha' : sᶜ ∈ 𝓝 a := by rwa [← mem_interior_iff_mem_nhds, interior_compl]
case tfae_4_to_2.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
tfae_6_to_4 :
  (∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a) → ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
H : ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
s : Set X
a : X
ha : ¬a ∈ closure s
ha' : sᶜ ∈ 𝓝 a
U : Set X
hU : U ∈ 𝓝 a
hUc : IsClosed U
hUs : U ⊆ sᶜ
⊢ Disjoint (𝓝ˢ s) (𝓝 a)
case tfae_4_to_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
tfae_6_to_4 :
  (∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a) → ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
H : ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
s : Set X
a : X
ha : ¬a ∈ closure s
ha' : sᶜ ∈ 𝓝 a
⊢ Disjoint (𝓝ˢ s) (𝓝 a)
rcases H _ _ ha' with ⟨U, hU, hUc, hUs⟩
case tfae_4_to_2.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
tfae_6_to_4 :
  (∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a) → ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
H : ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
s : Set X
a : X
ha : ¬a ∈ closure s
ha' : sᶜ ∈ 𝓝 a
U : Set X
hU : U ∈ 𝓝 a
hUc : IsClosed U
hUs : U ⊆ sᶜ
⊢ Uᶜ ∈ 𝓝ˢ s
case tfae_4_to_2.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
tfae_6_to_4 :
  (∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a) → ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
H : ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
s : Set X
a : X
ha : ¬a ∈ closure s
ha' : sᶜ ∈ 𝓝 a
U : Set X
hU : U ∈ 𝓝 a
hUc : IsClosed U
hUs : U ⊆ sᶜ
⊢ Disjoint (𝓝ˢ s) (𝓝 a)
refine' disjoint_of_disjoint_of_mem disjoint_compl_left _ hU
no goals
case tfae_4_to_2.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
tfae_6_to_4 :
  (∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a) → ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
H : ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
s : Set X
a : X
ha : ¬a ∈ closure s
ha' : sᶜ ∈ 𝓝 a
U : Set X
hU : U ∈ 𝓝 a
hUc : IsClosed U
hUs : U ⊆ sᶜ
⊢ Uᶜ ∈ 𝓝ˢ s
rwa [← subset_interior_iff_mem_nhdsSet, hUc.isOpen_compl.interior_eq, subset_compl_comm]
no goals
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
tfae_6_to_4 :
  (∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a) → ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
H : ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
s : Set X
a : X
ha : ¬a ∈ closure s
⊢ sᶜ ∈ 𝓝 a
rwa [← mem_interior_iff_mem_nhds, interior_compl]
case tfae_2_to_3
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
tfae_6_to_4 :
  (∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a) → ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
tfae_4_to_2 :
  (∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s) →
    ∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a)
H : ∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a)
a : X
s : Set X
hd : Disjoint (𝓝ˢ s) (𝓝 a)
has : a ∈ closure s
⊢ 𝓝 a ⊓ 𝓟 s = ⊥
case tfae_2_to_3
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
tfae_6_to_4 :
  (∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a) → ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
tfae_4_to_2 :
  (∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s) →
    ∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a)
⊢ (∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a)) →
    ∀ (a : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 a) ↔ ¬a ∈ closure s
refine' fun H a s => ⟨fun hd has => mem_closure_iff_nhds_neBot.mp has _, H s a⟩
no goals
case tfae_2_to_3
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
tfae_6_to_4 :
  (∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a) → ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
tfae_4_to_2 :
  (∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s) →
    ∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a)
H : ∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a)
a : X
s : Set X
hd : Disjoint (𝓝ˢ s) (𝓝 a)
has : a ∈ closure s
⊢ 𝓝 a ⊓ 𝓟 s = ⊥
exact (hd.symm.mono_right <| @principal_le_nhdsSet _ _ s).eq_bot
no goals
case tfae_3_to_1
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a
tfae_5_to_6 : (∀ (a : X), Filter.lift' (𝓝 a) closure ≤ 𝓝 a) → ∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a
tfae_6_to_4 :
  (∀ (a : X), Filter.lift' (𝓝 a) closure = 𝓝 a) → ∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
tfae_4_to_2 :
  (∀ (a : X) (s : Set X), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s) →
    ∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a)
tfae_2_to_3 :
  (∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (𝓝ˢ s) (𝓝 a)) →
    ∀ (a : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 a) ↔ ¬a ∈ closure s
⊢ (∀ (a : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 a) ↔ ¬a ∈ closure s) → RegularSpace X
exact fun H => ⟨fun hs ha => (H _ _).mpr <| hs.closure_eq.symm ▸ ha⟩