case tfae_1_iff_2
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
⊢ T1Space α ↔ ∀ (x : α), IsClosed {x}

α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
⊢ List.TFAE
    [T1Space α, ∀ (x : α), IsClosed {x}, ∀ (x : α), IsOpen ({x}ᶜ), Continuous ↑CofiniteTopology.of,
      ∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s,
      ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U, ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : α⦄, x ⤳ y → x = y]
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
⊢ List.TFAE
    [T1Space α, ∀ (x : α), IsClosed {x}, ∀ (x : α), IsOpen ({x}ᶜ), Continuous ↑CofiniteTopology.of,
      ∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s,
      ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U, ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : α⦄, x ⤳ y → x = y]
tfae_have 1 ↔ 2
case tfae_2_iff_3
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
⊢ (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)

α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
⊢ List.TFAE
    [T1Space α, ∀ (x : α), IsClosed {x}, ∀ (x : α), IsOpen ({x}ᶜ), Continuous ↑CofiniteTopology.of,
      ∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s,
      ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U, ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : α⦄, x ⤳ y → x = y]
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
⊢ List.TFAE
    [T1Space α, ∀ (x : α), IsClosed {x}, ∀ (x : α), IsOpen ({x}ᶜ), Continuous ↑CofiniteTopology.of,
      ∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s,
      ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U, ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : α⦄, x ⤳ y → x = y]
tfae_have 2 ↔ 3
case tfae_5_iff_3
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
⊢ (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)

α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
⊢ List.TFAE
    [T1Space α, ∀ (x : α), IsClosed {x}, ∀ (x : α), IsOpen ({x}ᶜ), Continuous ↑CofiniteTopology.of,
      ∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s,
      ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U, ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : α⦄, x ⤳ y → x = y]
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
⊢ List.TFAE
    [T1Space α, ∀ (x : α), IsClosed {x}, ∀ (x : α), IsOpen ({x}ᶜ), Continuous ↑CofiniteTopology.of,
      ∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s,
      ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U, ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : α⦄, x ⤳ y → x = y]
tfae_have 5 ↔ 3
case tfae_5_iff_6
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
⊢ (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s

α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_6 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
⊢ List.TFAE
    [T1Space α, ∀ (x : α), IsClosed {x}, ∀ (x : α), IsOpen ({x}ᶜ), Continuous ↑CofiniteTopology.of,
      ∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s,
      ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U, ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : α⦄, x ⤳ y → x = y]
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
⊢ List.TFAE
    [T1Space α, ∀ (x : α), IsClosed {x}, ∀ (x : α), IsOpen ({x}ᶜ), Continuous ↑CofiniteTopology.of,
      ∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s,
      ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U, ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : α⦄, x ⤳ y → x = y]
tfae_have 5 ↔ 6
case tfae_5_iff_7
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_6 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
⊢ (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U

α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_6 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
tfae_5_iff_7 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U
⊢ List.TFAE
    [T1Space α, ∀ (x : α), IsClosed {x}, ∀ (x : α), IsOpen ({x}ᶜ), Continuous ↑CofiniteTopology.of,
      ∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s,
      ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U, ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : α⦄, x ⤳ y → x = y]
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_6 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
⊢ List.TFAE
    [T1Space α, ∀ (x : α), IsClosed {x}, ∀ (x : α), IsOpen ({x}ᶜ), Continuous ↑CofiniteTopology.of,
      ∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s,
      ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U, ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : α⦄, x ⤳ y → x = y]
tfae_have 5 ↔ 7
case tfae_5_iff_8
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_6 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
tfae_5_iff_7 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U
⊢ (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)

α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_6 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
tfae_5_iff_7 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U
tfae_5_iff_8 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
⊢ List.TFAE
    [T1Space α, ∀ (x : α), IsClosed {x}, ∀ (x : α), IsOpen ({x}ᶜ), Continuous ↑CofiniteTopology.of,
      ∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s,
      ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U, ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : α⦄, x ⤳ y → x = y]
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_6 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
tfae_5_iff_7 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U
⊢ List.TFAE
    [T1Space α, ∀ (x : α), IsClosed {x}, ∀ (x : α), IsOpen ({x}ᶜ), Continuous ↑CofiniteTopology.of,
      ∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s,
      ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U, ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : α⦄, x ⤳ y → x = y]
tfae_have 5 ↔ 8
case tfae_8_iff_9
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_6 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
tfae_5_iff_7 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U
tfae_5_iff_8 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
⊢ (∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y)

α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_6 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
tfae_5_iff_7 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U
tfae_5_iff_8 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
⊢ List.TFAE
    [T1Space α, ∀ (x : α), IsClosed {x}, ∀ (x : α), IsOpen ({x}ᶜ), Continuous ↑CofiniteTopology.of,
      ∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s,
      ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U, ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : α⦄, x ⤳ y → x = y]
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_6 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
tfae_5_iff_7 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U
tfae_5_iff_8 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
⊢ List.TFAE
    [T1Space α, ∀ (x : α), IsClosed {x}, ∀ (x : α), IsOpen ({x}ᶜ), Continuous ↑CofiniteTopology.of,
      ∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s,
      ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U, ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : α⦄, x ⤳ y → x = y]
tfae_have 8 ↔ 9
case tfae_1_to_4
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_6 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
tfae_5_iff_7 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U
tfae_5_iff_8 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
⊢ T1Space α → Continuous ↑CofiniteTopology.of

α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_6 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
tfae_5_iff_7 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U
tfae_5_iff_8 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
tfae_1_to_4 : T1Space α → Continuous ↑CofiniteTopology.of
⊢ List.TFAE
    [T1Space α, ∀ (x : α), IsClosed {x}, ∀ (x : α), IsOpen ({x}ᶜ), Continuous ↑CofiniteTopology.of,
      ∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s,
      ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U, ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : α⦄, x ⤳ y → x = y]
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_6 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
tfae_5_iff_7 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U
tfae_5_iff_8 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
⊢ List.TFAE
    [T1Space α, ∀ (x : α), IsClosed {x}, ∀ (x : α), IsOpen ({x}ᶜ), Continuous ↑CofiniteTopology.of,
      ∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s,
      ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U, ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : α⦄, x ⤳ y → x = y]
tfae_have 1 → 4
case tfae_4_to_2
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_6 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
tfae_5_iff_7 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U
tfae_5_iff_8 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
tfae_1_to_4 : T1Space α → Continuous ↑CofiniteTopology.of
⊢ Continuous ↑CofiniteTopology.of → ∀ (x : α), IsClosed {x}

α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_6 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
tfae_5_iff_7 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U
tfae_5_iff_8 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
tfae_1_to_4 : T1Space α → Continuous ↑CofiniteTopology.of
tfae_4_to_2 : Continuous ↑CofiniteTopology.of → ∀ (x : α), IsClosed {x}
⊢ List.TFAE
    [T1Space α, ∀ (x : α), IsClosed {x}, ∀ (x : α), IsOpen ({x}ᶜ), Continuous ↑CofiniteTopology.of,
      ∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s,
      ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U, ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : α⦄, x ⤳ y → x = y]
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_6 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
tfae_5_iff_7 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U
tfae_5_iff_8 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
tfae_1_to_4 : T1Space α → Continuous ↑CofiniteTopology.of
⊢ List.TFAE
    [T1Space α, ∀ (x : α), IsClosed {x}, ∀ (x : α), IsOpen ({x}ᶜ), Continuous ↑CofiniteTopology.of,
      ∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s,
      ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U, ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : α⦄, x ⤳ y → x = y]
tfae_have 4 → 2
case tfae_2_iff_10
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_6 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
tfae_5_iff_7 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U
tfae_5_iff_8 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
tfae_1_to_4 : T1Space α → Continuous ↑CofiniteTopology.of
tfae_4_to_2 : Continuous ↑CofiniteTopology.of → ∀ (x : α), IsClosed {x}
⊢ (∀ (x : α), IsClosed {x}) ↔ ∀ ⦃x y : α⦄, x ⤳ y → x = y

α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_6 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
tfae_5_iff_7 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U
tfae_5_iff_8 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
tfae_1_to_4 : T1Space α → Continuous ↑CofiniteTopology.of
tfae_4_to_2 : Continuous ↑CofiniteTopology.of → ∀ (x : α), IsClosed {x}
tfae_2_iff_10 : (∀ (x : α), IsClosed {x}) ↔ ∀ ⦃x y : α⦄, x ⤳ y → x = y
⊢ List.TFAE
    [T1Space α, ∀ (x : α), IsClosed {x}, ∀ (x : α), IsOpen ({x}ᶜ), Continuous ↑CofiniteTopology.of,
      ∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s,
      ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U, ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : α⦄, x ⤳ y → x = y]
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_6 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
tfae_5_iff_7 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U
tfae_5_iff_8 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
tfae_1_to_4 : T1Space α → Continuous ↑CofiniteTopology.of
tfae_4_to_2 : Continuous ↑CofiniteTopology.of → ∀ (x : α), IsClosed {x}
⊢ List.TFAE
    [T1Space α, ∀ (x : α), IsClosed {x}, ∀ (x : α), IsOpen ({x}ᶜ), Continuous ↑CofiniteTopology.of,
      ∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s,
      ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U, ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : α⦄, x ⤳ y → x = y]
tfae_have 2 ↔ 10
no goals
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_6 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
tfae_5_iff_7 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U
tfae_5_iff_8 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
tfae_1_to_4 : T1Space α → Continuous ↑CofiniteTopology.of
tfae_4_to_2 : Continuous ↑CofiniteTopology.of → ∀ (x : α), IsClosed {x}
tfae_2_iff_10 : (∀ (x : α), IsClosed {x}) ↔ ∀ ⦃x y : α⦄, x ⤳ y → x = y
⊢ List.TFAE
    [T1Space α, ∀ (x : α), IsClosed {x}, ∀ (x : α), IsOpen ({x}ᶜ), Continuous ↑CofiniteTopology.of,
      ∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s,
      ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U, ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : α⦄, x ⤳ y → x = y]
tfae_finish
no goals
case tfae_1_iff_2
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
⊢ T1Space α ↔ ∀ (x : α), IsClosed {x}
exact ⟨fun h => h.1, fun h => ⟨h⟩⟩
no goals
case tfae_2_iff_3
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
⊢ (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
simp only [isOpen_compl_iff]
case tfae_5_iff_3
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
⊢ (∀ (y x : α), x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
case tfae_5_iff_3
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
⊢ (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
refine' forall_swap.trans _
no goals
case tfae_5_iff_3
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
⊢ (∀ (y x : α), x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
simp only [isOpen_iff_mem_nhds, mem_compl_iff, mem_singleton_iff]
no goals
case tfae_5_iff_6
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
⊢ (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
simp only [← subset_compl_singleton_iff, exists_mem_subset_iff]
no goals
case tfae_5_iff_7
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_6 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
⊢ (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U
simp only [(nhds_basis_opens _).mem_iff, subset_compl_singleton_iff, exists_prop, and_assoc,
  and_left_comm]
no goals
case tfae_5_iff_8
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_6 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
tfae_5_iff_7 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U
⊢ (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
simp only [← principal_singleton, disjoint_principal_right]
no goals
case tfae_8_iff_9
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_6 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
tfae_5_iff_7 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U
tfae_5_iff_8 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
⊢ (∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
exact forall_swap.trans (by simp only [disjoint_comm, ne_comm])
no goals
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_6 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
tfae_5_iff_7 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U
tfae_5_iff_8 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
⊢ (∀ (y x : α), x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
simp only [disjoint_comm, ne_comm]
case tfae_1_to_4
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_6 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
tfae_5_iff_7 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U
tfae_5_iff_8 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
⊢ T1Space α → ∀ (s : Set (CofiniteTopology α)), s = ∅ ∨ Set.Finite (sᶜ) → IsOpen (↑CofiniteTopology.of ⁻¹' s)
case tfae_1_to_4
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_6 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
tfae_5_iff_7 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U
tfae_5_iff_8 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
⊢ T1Space α → Continuous ↑CofiniteTopology.of
simp only [continuous_def, CofiniteTopology.isOpen_iff']
case tfae_1_to_4.inl
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_6 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
tfae_5_iff_7 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U
tfae_5_iff_8 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
H : T1Space α
⊢ IsOpen (↑CofiniteTopology.of ⁻¹' ∅)

case tfae_1_to_4.inr
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_6 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
tfae_5_iff_7 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U
tfae_5_iff_8 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
H : T1Space α
s : Set (CofiniteTopology α)
hs : Set.Finite (sᶜ)
⊢ IsOpen (↑CofiniteTopology.of ⁻¹' s)
case tfae_1_to_4
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_6 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
tfae_5_iff_7 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U
tfae_5_iff_8 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
⊢ T1Space α → ∀ (s : Set (CofiniteTopology α)), s = ∅ ∨ Set.Finite (sᶜ) → IsOpen (↑CofiniteTopology.of ⁻¹' s)
rintro H s (rfl | hs)
no goals
case tfae_1_to_4.inl
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_6 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
tfae_5_iff_7 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U
tfae_5_iff_8 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
H : T1Space α
⊢ IsOpen (↑CofiniteTopology.of ⁻¹' ∅)

case tfae_1_to_4.inr
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_6 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
tfae_5_iff_7 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U
tfae_5_iff_8 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
H : T1Space α
s : Set (CofiniteTopology α)
hs : Set.Finite (sᶜ)
⊢ IsOpen (↑CofiniteTopology.of ⁻¹' s)
exacts [isOpen_empty, compl_compl s ▸ (@Set.Finite.isClosed _ _ H _ hs).isOpen_compl]
no goals
case tfae_4_to_2
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_6 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
tfae_5_iff_7 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U
tfae_5_iff_8 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
tfae_1_to_4 : T1Space α → Continuous ↑CofiniteTopology.of
⊢ Continuous ↑CofiniteTopology.of → ∀ (x : α), IsClosed {x}
exact fun h x => (CofiniteTopology.isClosed_iff.2 <| Or.inr (finite_singleton _)).preimage h
no goals
case tfae_2_iff_10
α✝ : Type u
β : Type v
inst✝¹ : TopologicalSpace α✝
α : Type u
inst✝ : TopologicalSpace α
tfae_1_iff_2 : T1Space α ↔ ∀ (x : α), IsClosed {x}
tfae_2_iff_3 : (∀ (x : α), IsClosed {x}) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_3 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : α), IsOpen ({x}ᶜ)
tfae_5_iff_6 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ 𝓝 x ∧ ¬y ∈ s
tfae_5_iff_7 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U
tfae_5_iff_8 : (∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : α⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
tfae_1_to_4 : T1Space α → Continuous ↑CofiniteTopology.of
tfae_4_to_2 : Continuous ↑CofiniteTopology.of → ∀ (x : α), IsClosed {x}
⊢ (∀ (x : α), IsClosed {x}) ↔ ∀ ⦃x y : α⦄, x ⤳ y → x = y
simp only [← closure_subset_iff_isClosed, specializes_iff_mem_closure, subset_def,
  mem_singleton_iff, eq_comm]