case pos
α : Type ?u.110881
β : Type ?u.110884
γ : Type ?u.110887
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
a : ℝ≥0∞
a_infty : a = ⊤
⊢ Continuous fun x => x - a

case neg
α : Type ?u.110881
β : Type ?u.110884
γ : Type ?u.110887
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
a : ℝ≥0∞
a_infty : ¬a = ⊤
⊢ Continuous fun x => x - a
α : Type ?u.110881
β : Type ?u.110884
γ : Type ?u.110887
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
a : ℝ≥0∞
⊢ Continuous fun x => x - a
by_cases a_infty : a = ∞
no goals
case pos
α : Type ?u.110881
β : Type ?u.110884
γ : Type ?u.110887
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
a : ℝ≥0∞
a_infty : a = ⊤
⊢ Continuous fun x => x - a
simp [a_infty, continuous_const]
case neg
α : Type ?u.110881
β : Type ?u.110884
γ : Type ?u.110887
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
a : ℝ≥0∞
a_infty : ¬a = ⊤
⊢ Continuous ((fun p => p.fst - p.snd) ∘ fun x => (x, a))
case neg
α : Type ?u.110881
β : Type ?u.110884
γ : Type ?u.110887
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
a : ℝ≥0∞
a_infty : ¬a = ⊤
⊢ Continuous fun x => x - a
rw [show (fun x => x - a) = (fun p : ℝ≥0∞ × ℝ≥0∞ => p.fst - p.snd) ∘ fun x => ⟨x, a⟩ by rfl]
case neg
α : Type ?u.110881
β : Type ?u.110884
γ : Type ?u.110887
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
a : ℝ≥0∞
a_infty : ¬a = ⊤
⊢ ∀ (x : ℝ≥0∞), (x, a) ∈ {p | p ≠ (⊤, ⊤)}
case neg
α : Type ?u.110881
β : Type ?u.110884
γ : Type ?u.110887
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
a : ℝ≥0∞
a_infty : ¬a = ⊤
⊢ Continuous ((fun p => p.fst - p.snd) ∘ fun x => (x, a))
apply ContinuousOn.comp_continuous continuousOn_sub (continuous_id'.prod_mk continuous_const)
case neg
α : Type ?u.110881
β : Type ?u.110884
γ : Type ?u.110887
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
a : ℝ≥0∞
a_infty : ¬a = ⊤
x : ℝ≥0∞
⊢ (x, a) ∈ {p | p ≠ (⊤, ⊤)}
case neg
α : Type ?u.110881
β : Type ?u.110884
γ : Type ?u.110887
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
a : ℝ≥0∞
a_infty : ¬a = ⊤
⊢ ∀ (x : ℝ≥0∞), (x, a) ∈ {p | p ≠ (⊤, ⊤)}
intro x
no goals
case neg
α : Type ?u.110881
β : Type ?u.110884
γ : Type ?u.110887
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
a : ℝ≥0∞
a_infty : ¬a = ⊤
x : ℝ≥0∞
⊢ (x, a) ∈ {p | p ≠ (⊤, ⊤)}
simp only [a_infty, Ne.def, mem_setOf_eq, Prod.mk.inj_iff, and_false_iff, not_false_iff]
no goals
α : Type ?u.110881
β : Type ?u.110884
γ : Type ?u.110887
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
a : ℝ≥0∞
a_infty : ¬a = ⊤
⊢ (fun x => x - a) = (fun p => p.fst - p.snd) ∘ fun x => (x, a)
rfl