[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (↑f) 0 s
hft : EqOn (↑f) 1 t
hf01 : ∀ (x : X), ↑f x ∈ Icc 0 1
x : X
hx : x ∈ s
⊢ ↑(BoundedContinuousFunction.const X a + (b - a) • f) x = Function.const X a x
[PROOFSTEP]
simp [hfs hx]
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (↑f) 0 s
hft : EqOn (↑f) 1 t
hf01 : ∀ (x : X), ↑f x ∈ Icc 0 1
x : X
hx : x ∈ t
⊢ ↑(BoundedContinuousFunction.const X a + (b - a) • f) x = Function.const X b x
[PROOFSTEP]
simp [hft hx]
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (↑f) 0 s
hft : EqOn (↑f) 1 t
hf01 : ∀ (x : X), ↑f x ∈ Icc 0 1
x : X
⊢ a ≤ ↑(BoundedContinuousFunction.const X a + (b - a) • f) x
[PROOFSTEP]
dsimp
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (↑f) 0 s
hft : EqOn (↑f) 1 t
hf01 : ∀ (x : X), ↑f x ∈ Icc 0 1
x : X
⊢ a ≤ a + (b - a) * ↑f x
[PROOFSTEP]
nlinarith [(hf01 x).1]
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (↑f) 0 s
hft : EqOn (↑f) 1 t
hf01 : ∀ (x : X), ↑f x ∈ Icc 0 1
x : X
⊢ ↑(BoundedContinuousFunction.const X a + (b - a) • f) x ≤ b
[PROOFSTEP]
dsimp
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (↑f) 0 s
hft : EqOn (↑f) 1 t
hf01 : ∀ (x : X), ↑f x ∈ Icc 0 1
x : X
⊢ a + (b - a) * ↑f x ≤ b
[PROOFSTEP]
nlinarith [(hf01 x).2]
