X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K : Compacts X
⊢ Set.Nonempty {f | ∀ (x : X), x ∈ K → 1 ≤ ↑f x}
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K : Compacts X
⊢ Set.Nonempty (↑Λ '' {f | ∀ (x : X), x ∈ K → 1 ≤ ↑f x})
rw [nonempty_image_iff]
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K : Compacts X
⊢ 1 ∈ {f | ∀ (x : X), x ∈ K → 1 ≤ ↑f x}
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K : Compacts X
⊢ Set.Nonempty {f | ∀ (x : X), x ∈ K → 1 ≤ ↑f x}
use (1 : X →ᵇ ℝ≥0)
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K : Compacts X
x : X
a✝ : x ∈ K
⊢ 1 ≤ ↑1 x
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K : Compacts X
⊢ 1 ∈ {f | ∀ (x : X), x ∈ K → 1 ≤ ↑f x}
intro x _
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K : Compacts X
x : X
a✝ : x ∈ K
⊢ 1 ≤ 1
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K : Compacts X
x : X
a✝ : x ∈ K
⊢ 1 ≤ ↑1 x
simp only [BoundedContinuousFunction.coe_one, Pi.one_apply]
no goals
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K : Compacts X
x : X
a✝ : x ∈ K
⊢ 1 ≤ 1
rfl