α : Type u
inst✝⁵ : TopologicalSpace α
γ : Type u
inst✝⁴ : TopologicalSpace γ
inst✝³ : T2Space γ
inst✝² : CompactSpace γ
γ' : Type u
inst✝¹ : TopologicalSpace γ'
inst✝ : T2Space γ'
f : α → γ
hf : Continuous f
g₁ g₂ : StoneCech α → γ'
h₁ : Continuous g₁
h₂ : Continuous g₂
h : g₁ ∘ stoneCechUnit = g₂ ∘ stoneCechUnit
⊢ EqOn g₁ g₂ (range stoneCechUnit)
α : Type u
inst✝⁵ : TopologicalSpace α
γ : Type u
inst✝⁴ : TopologicalSpace γ
inst✝³ : T2Space γ
inst✝² : CompactSpace γ
γ' : Type u
inst✝¹ : TopologicalSpace γ'
inst✝ : T2Space γ'
f : α → γ
hf : Continuous f
g₁ g₂ : StoneCech α → γ'
h₁ : Continuous g₁
h₂ : Continuous g₂
h : g₁ ∘ stoneCechUnit = g₂ ∘ stoneCechUnit
⊢ g₁ = g₂
apply Continuous.ext_on denseRange_stoneCechUnit h₁ h₂
case intro
α : Type u
inst✝⁵ : TopologicalSpace α
γ : Type u
inst✝⁴ : TopologicalSpace γ
inst✝³ : T2Space γ
inst✝² : CompactSpace γ
γ' : Type u
inst✝¹ : TopologicalSpace γ'
inst✝ : T2Space γ'
f : α → γ
hf : Continuous f
g₁ g₂ : StoneCech α → γ'
h₁ : Continuous g₁
h₂ : Continuous g₂
h : g₁ ∘ stoneCechUnit = g₂ ∘ stoneCechUnit
x : α
⊢ g₁ (stoneCechUnit x) = g₂ (stoneCechUnit x)
α : Type u
inst✝⁵ : TopologicalSpace α
γ : Type u
inst✝⁴ : TopologicalSpace γ
inst✝³ : T2Space γ
inst✝² : CompactSpace γ
γ' : Type u
inst✝¹ : TopologicalSpace γ'
inst✝ : T2Space γ'
f : α → γ
hf : Continuous f
g₁ g₂ : StoneCech α → γ'
h₁ : Continuous g₁
h₂ : Continuous g₂
h : g₁ ∘ stoneCechUnit = g₂ ∘ stoneCechUnit
⊢ EqOn g₁ g₂ (range stoneCechUnit)
rintro x ⟨x, rfl⟩
no goals
case intro
α : Type u
inst✝⁵ : TopologicalSpace α
γ : Type u
inst✝⁴ : TopologicalSpace γ
inst✝³ : T2Space γ
inst✝² : CompactSpace γ
γ' : Type u
inst✝¹ : TopologicalSpace γ'
inst✝ : T2Space γ'
f : α → γ
hf : Continuous f
g₁ g₂ : StoneCech α → γ'
h₁ : Continuous g₁
h₂ : Continuous g₂
h : g₁ ∘ stoneCechUnit = g₂ ∘ stoneCechUnit
x : α
⊢ g₁ (stoneCechUnit x) = g₂ (stoneCechUnit x)
apply congr_fun h x