α : Type ?u.110099
β : Type ?u.110102
γ : Type ?u.110105
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
a : ℝ≥0∞
⊢ ContinuousOn ((fun p => p.fst - p.snd) ∘ fun x => (a, x)) {x | x ≠ ⊤}
α : Type ?u.110099
β : Type ?u.110102
γ : Type ?u.110105
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
a : ℝ≥0∞
⊢ ContinuousOn (fun x => a - x) {x | x ≠ ⊤}
rw [show (fun x => a - x) = (fun p : ℝ≥0∞ × ℝ≥0∞ => p.fst - p.snd) ∘ fun x => ⟨a, x⟩ by rfl]
α : Type ?u.110099
β : Type ?u.110102
γ : Type ?u.110105
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
a : ℝ≥0∞
⊢ MapsTo (fun b => (a, b)) {x | x ≠ ⊤} {p | p ≠ (⊤, ⊤)}
α : Type ?u.110099
β : Type ?u.110102
γ : Type ?u.110105
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
a : ℝ≥0∞
⊢ ContinuousOn ((fun p => p.fst - p.snd) ∘ fun x => (a, x)) {x | x ≠ ⊤}
apply ContinuousOn.comp continuousOn_sub (Continuous.continuousOn (Continuous.Prod.mk a))
case refl
α : Type ?u.110099
β : Type ?u.110102
γ : Type ?u.110105
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
h : ⊤ ∈ {x | x ≠ ⊤}
⊢ False
α : Type ?u.110099
β : Type ?u.110102
γ : Type ?u.110105
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
a : ℝ≥0∞
⊢ MapsTo (fun b => (a, b)) {x | x ≠ ⊤} {p | p ≠ (⊤, ⊤)}
rintro _ h (_ | _)
no goals
case refl
α : Type ?u.110099
β : Type ?u.110102
γ : Type ?u.110105
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
h : ⊤ ∈ {x | x ≠ ⊤}
⊢ False
exact h none_eq_top
no goals
α : Type ?u.110099
β : Type ?u.110102
γ : Type ?u.110105
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
a : ℝ≥0∞
⊢ (fun x => a - x) = (fun p => p.fst - p.snd) ∘ fun x => (a, x)
rfl