case mp
X Y : CompHaus
f : X ⟶ Y
⊢ Epi f → Function.Surjective ((forget CompHaus).map f)

case mpr
X Y : CompHaus
f : X ⟶ Y
⊢ Function.Surjective ((forget CompHaus).map f) → Epi f
X Y : CompHaus
f : X ⟶ Y
⊢ Epi f ↔ Function.Surjective ((forget CompHaus).map f)
constructor
case mp
X Y : CompHaus
f : X ⟶ Y
⊢ Epi f → ∀ (b : (forget CompHaus).obj Y), ∃ a, (forget CompHaus).map f a = b
case mp
X Y : CompHaus
f : X ⟶ Y
⊢ Epi f → Function.Surjective ((forget CompHaus).map f)
dsimp [Function.Surjective]
case mp
X Y : CompHaus
f : X ⟶ Y
⊢ (∃ b, ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ b) → ¬Epi f
case mp
X Y : CompHaus
f : X ⟶ Y
⊢ Epi f → ∀ (b : (forget CompHaus).obj Y), ∃ a, (forget CompHaus).map f a = b
contrapose!
case mp.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
⊢ False
case mp
X Y : CompHaus
f : X ⟶ Y
⊢ (∃ b, ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ b) → ¬Epi f
rintro ⟨y, hy⟩ hf
case mp.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
⊢ False
case mp.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
⊢ False
let C := Set.range f
case mp.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
⊢ False
case mp.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
⊢ False
have hC : IsClosed C := (isCompact_range f.continuous).isClosed
case mp.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
⊢ False
case mp.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
⊢ False
let D := ({y} : Set Y)
case mp.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
⊢ False
case mp.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
⊢ False
have hD : IsClosed D := isClosed_singleton
case mp.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
⊢ False
case mp.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
⊢ False
have hCD : Disjoint C D := by
  rw [Set.disjoint_singleton_right]
  rintro ⟨y', hy'⟩
  exact hy y' hy'
case mp.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this : NormalSpace ((forget CompHaus).obj Y)
⊢ False
case mp.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
⊢ False
haveI : NormalSpace ((forget CompHaus).obj Y) := normalOfCompactT2
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
⊢ False
case mp.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this : NormalSpace ((forget CompHaus).obj Y)
⊢ False
obtain ⟨φ, hφ0, hφ1, hφ01⟩ := exists_continuous_zero_one_of_closed hC hD hCD
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this : CompactSpace (ULift ↑(Set.Icc 0 1))
⊢ False
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
⊢ False
haveI : CompactSpace (ULift.{u} <| Set.Icc (0 : ℝ) 1) := Homeomorph.ulift.symm.compactSpace
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
⊢ False
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this : CompactSpace (ULift ↑(Set.Icc 0 1))
⊢ False
haveI : T2Space (ULift.{u} <| Set.Icc (0 : ℝ) 1) := Homeomorph.ulift.symm.t2Space
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
⊢ False
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
⊢ False
let Z := of (ULift.{u} <| Set.Icc (0 : ℝ) 1)
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
⊢ False
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
⊢ False
let g : Y ⟶ Z :=
  ⟨fun y' => ⟨⟨φ y', hφ01 y'⟩⟩,
    continuous_uLift_up.comp (φ.continuous.subtype_mk fun y' => hφ01 y')⟩
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
⊢ False
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
⊢ False
let h : Y ⟶ Z := ⟨fun _ => ⟨⟨0, Set.left_mem_Icc.mpr zero_le_one⟩⟩, continuous_const⟩
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
H : h = g
⊢ False
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
⊢ False
have H : h = g := by
  rw [← cancel_epi f]
  ext x
  apply ULift.ext
  apply Subtype.ext
  dsimp
  change 0 = φ (f x)
  simp only [hφ0 (Set.mem_range_self x), Pi.zero_apply]
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
H : ↑((forget CompHaus).map h y).down = ↑((forget CompHaus).map g y).down
⊢ False
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
H : h = g
⊢ False
apply_fun fun e => (e y).down.1 at H
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
H :
  ↑((forget CompHaus).map (ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } })
          y).down =
    ↑((forget CompHaus).map
          (ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }) y).down
⊢ False
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
H : ↑((forget CompHaus).map h y).down = ↑((forget CompHaus).map g y).down
⊢ False
dsimp at H
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
H : 0 = ↑φ y
⊢ False
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
H :
  ↑((forget CompHaus).map (ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } })
          y).down =
    ↑((forget CompHaus).map
          (ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }) y).down
⊢ False
change 0 = φ y at H
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
H : 0 = 1
⊢ False
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
H : 0 = ↑φ y
⊢ False
simp only [hφ1 (Set.mem_singleton y), Pi.one_apply] at H
no goals
case mp.intro.intro.intro.intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
H : 0 = 1
⊢ False
exact zero_ne_one H
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
⊢ ¬y ∈ C
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
⊢ Disjoint C D
rw [Set.disjoint_singleton_right]
case intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
y' : (forget CompHaus).obj X
hy' : (forget CompHaus).map f y' = y
⊢ False
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
⊢ ¬y ∈ C
rintro ⟨y', hy'⟩
no goals
case intro
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
y' : (forget CompHaus).obj X
hy' : (forget CompHaus).map f y' = y
⊢ False
exact hy y' hy'
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
⊢ f ≫ h = f ≫ g
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
⊢ h = g
rw [← cancel_epi f]
case w
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
x : (forget CompHaus).obj X
⊢ (forget CompHaus).map (f ≫ h) x = (forget CompHaus).map (f ≫ g) x
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
⊢ f ≫ h = f ≫ g
ext x
case w.h
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
x : (forget CompHaus).obj X
⊢ ((forget CompHaus).map (f ≫ h) x).down = ((forget CompHaus).map (f ≫ g) x).down
case w
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
x : (forget CompHaus).obj X
⊢ (forget CompHaus).map (f ≫ h) x = (forget CompHaus).map (f ≫ g) x
apply ULift.ext
case w.h.a
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
x : (forget CompHaus).obj X
⊢ ↑((forget CompHaus).map (f ≫ h) x).down = ↑((forget CompHaus).map (f ≫ g) x).down
case w.h
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
x : (forget CompHaus).obj X
⊢ ((forget CompHaus).map (f ≫ h) x).down = ((forget CompHaus).map (f ≫ g) x).down
apply Subtype.ext
case w.h.a
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
x : (forget CompHaus).obj X
⊢ ↑((forget CompHaus).map (f ≫ ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } })
          x).down =
    ↑((forget CompHaus).map
          (f ≫ ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }) x).down
case w.h.a
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
x : (forget CompHaus).obj X
⊢ ↑((forget CompHaus).map (f ≫ h) x).down = ↑((forget CompHaus).map (f ≫ g) x).down
dsimp
case w.h.a
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
x : (forget CompHaus).obj X
⊢ 0 = ↑φ ((forget CompHaus).map f x)
case w.h.a
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
x : (forget CompHaus).obj X
⊢ ↑((forget CompHaus).map (f ≫ ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } })
          x).down =
    ↑((forget CompHaus).map
          (f ≫ ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }) x).down
change 0 = φ (f x)
no goals
case w.h.a
X Y : CompHaus
f : X ⟶ Y
y : (forget CompHaus).obj Y
hy : ∀ (a : (forget CompHaus).obj X), (forget CompHaus).map f a ≠ y
hf : Epi f
C : Set ((forget CompHaus).obj Y) := Set.range ((forget CompHaus).map f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
this✝¹ : NormalSpace ((forget CompHaus).obj Y)
φ : C((forget CompHaus).obj Y, ℝ)
hφ0 : Set.EqOn (↑φ) 0 C
hφ1 : Set.EqOn (↑φ) 1 D
hφ01 : ∀ (x : (forget CompHaus).obj Y), ↑φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift ↑(Set.Icc 0 1))
this : T2Space (ULift ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift ↑(Set.Icc 0 1))
g : Y ⟶ Z := ContinuousMap.mk fun y' => { down := { val := ↑φ y', property := (_ : ↑φ y' ∈ Set.Icc 0 1) } }
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }
x : (forget CompHaus).obj X
⊢ 0 = ↑φ ((forget CompHaus).map f x)
simp only [hφ0 (Set.mem_range_self x), Pi.zero_apply]
case mpr
X Y : CompHaus
f : X ⟶ Y
⊢ Epi ((forget CompHaus).map f) → Epi f
case mpr
X Y : CompHaus
f : X ⟶ Y
⊢ Function.Surjective ((forget CompHaus).map f) → Epi f
rw [← CategoryTheory.epi_iff_surjective]
no goals
case mpr
X Y : CompHaus
f : X ⟶ Y
⊢ Epi ((forget CompHaus).map f) → Epi f
apply (forget CompHaus).epi_of_epi_map