Chase lean project

v1.lean

import topology.subset_properties
import topology.connected
import topology.nhds_set
import topology.inseparable
import topology.separation
import topology.maps

open function set filter topological_space
open_locale topological_space filter classical
                             

universes u v
variables {α : Type u} {β : Type v} [topological_space α]

open separated

def function_diagonal (f: α → β): set (α × α) := {p | f p.1 = f p.2}

lemma t2_closed_func_diag [t2_space α] [topological_space β] [f:β → α] (hf : continuous f): is_closed (function_diagonal f) :=
begin
  refine is_closed_iff_cluster_pt.mpr _,
  rintro ⟨ a₁, a₂ ⟩ h,
  refine eq_of_nhds_ne_bot ⟨ λ this : 𝓝 (f a₁) ⊓ 𝓝 (f a₂) = ⊥, h.ne _⟩,
  obtain ⟨ t₁, (ht₁ : t₁ ∈ 𝓝 (f a₁)), t₂, (ht₂ : t₂ ∈ 𝓝 (f a₂)), (h' : t₁ ∩ t₂ = ∅)⟩ :=
    inf_eq_bot_iff.mp this,
  obtain ha₁ := continuous_at.preimage_mem_nhds ((continuous_iff_continuous_at.mp hf) a₁) ht₁,
  obtain ha₂ := continuous_at.preimage_mem_nhds ((continuous_iff_continuous_at.mp hf) a₂) ht₂,
  rw [inf_principal_eq_bot, nhds_prod_eq],
  apply mem_of_superset (prod_mem_prod ha₁ ha₂),
  rintro ⟨x, y⟩ ⟨x_in, y_in⟩ (heq : f x = f y),
  dsimp at x_in y_in,
  /- Need to show x ∈ f⁻¹' t₂ from f x = f y by doing some rw ← heq at * or something -/
  have : x ∈ (f⁻¹' t₁) ∩ (f⁻¹' t₂),
  { dsimp,
    split,
    { assumption },
    { rw heq,
      assumption } },
  rw ← set.preimage_inter at this,
  rw h' at this,
  rw set.preimage_empty at this,
  apply set.not_mem_empty,
  exact this
end

v2.lean

import topology.subset_properties
import topology.connected
import topology.nhds_set
import topology.inseparable
import topology.separation
import topology.maps

open function set filter topological_space
open_locale topological_space filter classical
                             

universes u v
variables {α : Type u} {β : Type v} [topological_space α]

open separated

def function_diagonal (f: α → β): set (α × α) := {p | f p.1 = f p.2}

lemma t2_closed_func_diag [t2_space α] [topological_space β] [f:β → α] (hf : continuous f): is_closed (function_diagonal f) :=
begin
  refine is_closed_iff_cluster_pt.mpr _,
  rintro ⟨ a₁, a₂ ⟩ h,
  refine eq_of_nhds_ne_bot ⟨ λ this : 𝓝 (f a₁) ⊓ 𝓝 (f a₂) = ⊥, h.ne _⟩,
  obtain ⟨ t₁, (ht₁ : t₁ ∈ 𝓝 (f a₁)), t₂, (ht₂ : t₂ ∈ 𝓝 (f a₂)), (h' : t₁ ∩ t₂ = ∅)⟩ :=
    inf_eq_bot_iff.mp this,
  obtain ha₁ := continuous_at.preimage_mem_nhds ((continuous_iff_continuous_at.mp hf) a₁) ht₁,
  obtain ha₂ := continuous_at.preimage_mem_nhds ((continuous_iff_continuous_at.mp hf) a₂) ht₂,
  rw [inf_principal_eq_bot, nhds_prod_eq],
  apply mem_of_superset (prod_mem_prod ha₁ ha₂),
  rintro ⟨x, y⟩ ⟨x_in, y_in⟩ (heq : f x = f y),
  have : x ∈ (f⁻¹' t₁) ∩ (f⁻¹' t₂) := ⟨x_in, @eq.substr _ (λ z, z ∈ t₂) _ _ heq (y_in : f y ∈ t₂)⟩,
  rw ← set.preimage_inter at this,
  rw h' at this,
  rw set.preimage_empty at this,
  exact set.not_mem_empty _ this
end

v3.lean

import topology.subset_properties
import topology.connected
import topology.nhds_set
import topology.inseparable
import topology.separation
import topology.maps

open function set filter topological_space
open_locale topological_space filter classical
                             

universes u v
variables {α : Type u} {β : Type v} [topological_space α]

open separated

def function_diagonal (f: α → β): set (α × α) := {p | f p.1 = f p.2}

lemma t2_closed_func_diag [t2_space α] [topological_space β] [f:β → α] (hf : continuous f): is_closed (function_diagonal f) :=
begin
  refine is_closed_iff_cluster_pt.mpr _,
  rintro ⟨ a₁, a₂ ⟩ h,
  refine eq_of_nhds_ne_bot ⟨ λ this : 𝓝 (f a₁) ⊓ 𝓝 (f a₂) = ⊥, h.ne _⟩,
  obtain ⟨ t₁, (ht₁ : t₁ ∈ 𝓝 (f a₁)), t₂, (ht₂ : t₂ ∈ 𝓝 (f a₂)), (h' : t₁ ∩ t₂ = ∅)⟩ :=
    inf_eq_bot_iff.mp this,
  obtain ha₁ := continuous_at.preimage_mem_nhds ((continuous_iff_continuous_at.mp hf) a₁) ht₁,
  obtain ha₂ := continuous_at.preimage_mem_nhds ((continuous_iff_continuous_at.mp hf) a₂) ht₂,
  rw [inf_principal_eq_bot, nhds_prod_eq],
  apply mem_of_superset (prod_mem_prod ha₁ ha₂),
  rintro ⟨x, y⟩ ⟨x_in, y_in⟩ (heq : f x = f y),
  have : x ∈ (f⁻¹' t₁) ∩ (f⁻¹' t₂) := ⟨x_in, @eq.substr _ t₂ _ _ heq (y_in : f y ∈ t₂)⟩,
  rw ← set.preimage_inter at this,
  rw h' at this,
  rw set.preimage_empty at this,
  exact set.not_mem_empty _ this
end

v4.lean

import topology.subset_properties
import topology.connected
import topology.nhds_set
import topology.inseparable
import topology.separation
import topology.maps

open function set filter topological_space
open_locale topological_space filter classical
                             

universes u v
variables {α : Type u} {β : Type v} [topological_space α]

open separated

def function_diagonal (f: α → β): set (α × α) := {p | f p.1 = f p.2}

lemma t2_closed_func_diag [t2_space α] [topological_space β] [f:β → α] (hf : continuous f): is_closed (function_diagonal f) :=
begin
  refine is_closed_iff_cluster_pt.mpr _,
  rintro ⟨ a₁, a₂ ⟩ h,
  refine eq_of_nhds_ne_bot ⟨ λ this : 𝓝 (f a₁) ⊓ 𝓝 (f a₂) = ⊥, h.ne _⟩,
  obtain ⟨ t₁, (ht₁ : t₁ ∈ 𝓝 (f a₁)), t₂, (ht₂ : t₂ ∈ 𝓝 (f a₂)), (h' : t₁ ∩ t₂ = ∅)⟩ :=
    inf_eq_bot_iff.mp this,
  obtain ha₁ := continuous_at.preimage_mem_nhds ((continuous_iff_continuous_at.mp hf) a₁) ht₁,
  obtain ha₂ := continuous_at.preimage_mem_nhds ((continuous_iff_continuous_at.mp hf) a₂) ht₂,
  rw [inf_principal_eq_bot, nhds_prod_eq],
  apply mem_of_superset (prod_mem_prod ha₁ ha₂),
  rintro ⟨x, y⟩ ⟨x_in, y_in⟩ (heq : f x = f y),
  apply set.not_mem_empty x,
  rw ← @set.preimage_empty _ _ f,
  rw ← h',
  rw set.preimage_inter,
  split,
  { exact x_in },
  { rw mem_preimage,
    rw heq,
    exact y_in }
end