case intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K : Compacts X
ε : ℝ≥0
εpos : 0 < ε
α : ℝ≥0
α_hyp : α < rieszContentAux Λ K + ε
f : X →ᵇ ℝ≥0
f_hyp : f ∈ {f | ∀ (x : X), x ∈ K → 1 ≤ ↑f x} ∧ ↑Λ f = α
⊢ ∃ f, (∀ (x : X), x ∈ K → 1 ≤ ↑f x) ∧ ↑Λ f < rieszContentAux Λ K + ε
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K : Compacts X
ε : ℝ≥0
εpos : 0 < ε
⊢ ∃ f, (∀ (x : X), x ∈ K → 1 ≤ ↑f x) ∧ ↑Λ f < rieszContentAux Λ K + ε
obtain ⟨α, ⟨⟨f, f_hyp⟩, α_hyp⟩⟩ :=
  exists_lt_of_csInf_lt (riesz_content_aux_image_nonempty Λ K)
    (lt_add_of_pos_right (rieszContentAux Λ K) εpos)
case intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K : Compacts X
ε : ℝ≥0
εpos : 0 < ε
α : ℝ≥0
α_hyp : α < rieszContentAux Λ K + ε
f : X →ᵇ ℝ≥0
f_hyp : f ∈ {f | ∀ (x : X), x ∈ K → 1 ≤ ↑f x} ∧ ↑Λ f = α
⊢ ↑Λ f < rieszContentAux Λ K + ε
case intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K : Compacts X
ε : ℝ≥0
εpos : 0 < ε
α : ℝ≥0
α_hyp : α < rieszContentAux Λ K + ε
f : X →ᵇ ℝ≥0
f_hyp : f ∈ {f | ∀ (x : X), x ∈ K → 1 ≤ ↑f x} ∧ ↑Λ f = α
⊢ ∃ f, (∀ (x : X), x ∈ K → 1 ≤ ↑f x) ∧ ↑Λ f < rieszContentAux Λ K + ε
refine' ⟨f, f_hyp.left, _⟩
case intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K : Compacts X
ε : ℝ≥0
εpos : 0 < ε
α : ℝ≥0
α_hyp : α < rieszContentAux Λ K + ε
f : X →ᵇ ℝ≥0
f_hyp : f ∈ {f | ∀ (x : X), x ∈ K → 1 ≤ ↑f x} ∧ ↑Λ f = α
⊢ α < rieszContentAux Λ K + ε
case intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K : Compacts X
ε : ℝ≥0
εpos : 0 < ε
α : ℝ≥0
α_hyp : α < rieszContentAux Λ K + ε
f : X →ᵇ ℝ≥0
f_hyp : f ∈ {f | ∀ (x : X), x ∈ K → 1 ≤ ↑f x} ∧ ↑Λ f = α
⊢ ↑Λ f < rieszContentAux Λ K + ε
rw [f_hyp.right]
no goals
case intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K : Compacts X
ε : ℝ≥0
εpos : 0 < ε
α : ℝ≥0
α_hyp : α < rieszContentAux Λ K + ε
f : X →ᵇ ℝ≥0
f_hyp : f ∈ {f | ∀ (x : X), x ∈ K → 1 ≤ ↑f x} ∧ ↑Λ f = α
⊢ α < rieszContentAux Λ K + ε
exact α_hyp