case intro.intro
𝓕 : Type ?u.1239473
𝕜 : Type ?u.1239476
α : Type u_2
ι : Type ?u.1239482
κ : Type ?u.1239485
E : Type u_1
F : Type ?u.1239491
G : Type ?u.1239494
inst✝¹ : NormedAddGroup α
f : α → E
inst✝ : One E
hf : HasCompactMulSupport f
K : Set α
hK1 : IsCompact K
hK2 : ∀ (x : α), ¬x ∈ K → f x = 1
⊢ ∃ R, 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 1
𝓕 : Type ?u.1239473
𝕜 : Type ?u.1239476
α : Type u_2
ι : Type ?u.1239482
κ : Type ?u.1239485
E : Type u_1
F : Type ?u.1239491
G : Type ?u.1239494
inst✝¹ : NormedAddGroup α
f : α → E
inst✝ : One E
hf : HasCompactMulSupport f
⊢ ∃ R, 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 1
obtain ⟨K, ⟨hK1, hK2⟩⟩ := exists_compact_iff_hasCompactMulSupport.mpr hf
case intro.intro.intro.intro
𝓕 : Type ?u.1239473
𝕜 : Type ?u.1239476
α : Type u_2
ι : Type ?u.1239482
κ : Type ?u.1239485
E : Type u_1
F : Type ?u.1239491
G : Type ?u.1239494
inst✝¹ : NormedAddGroup α
f : α → E
inst✝ : One E
hf : HasCompactMulSupport f
K : Set α
hK1 : IsCompact K
hK2 : ∀ (x : α), ¬x ∈ K → f x = 1
S : ℝ
hS : S > 0
hS' : ∀ (x : α), x ∈ K → ‖x‖ ≤ S
⊢ ∃ R, 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 1
case intro.intro
𝓕 : Type ?u.1239473
𝕜 : Type ?u.1239476
α : Type u_2
ι : Type ?u.1239482
κ : Type ?u.1239485
E : Type u_1
F : Type ?u.1239491
G : Type ?u.1239494
inst✝¹ : NormedAddGroup α
f : α → E
inst✝ : One E
hf : HasCompactMulSupport f
K : Set α
hK1 : IsCompact K
hK2 : ∀ (x : α), ¬x ∈ K → f x = 1
⊢ ∃ R, 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 1
obtain ⟨S, hS, hS'⟩ := hK1.bounded.exists_pos_norm_le
case intro.intro.intro.intro
𝓕 : Type ?u.1239473
𝕜 : Type ?u.1239476
α : Type u_2
ι : Type ?u.1239482
κ : Type ?u.1239485
E : Type u_1
F : Type ?u.1239491
G : Type ?u.1239494
inst✝¹ : NormedAddGroup α
f : α → E
inst✝ : One E
hf : HasCompactMulSupport f
K : Set α
hK1 : IsCompact K
hK2 : ∀ (x : α), ¬x ∈ K → f x = 1
S : ℝ
hS : S > 0
hS' : ∀ (x : α), x ∈ K → ‖x‖ ≤ S
x : α
hx : S + 1 ≤ ‖x‖
⊢ ¬‖x‖ ≤ S
case intro.intro.intro.intro
𝓕 : Type ?u.1239473
𝕜 : Type ?u.1239476
α : Type u_2
ι : Type ?u.1239482
κ : Type ?u.1239485
E : Type u_1
F : Type ?u.1239491
G : Type ?u.1239494
inst✝¹ : NormedAddGroup α
f : α → E
inst✝ : One E
hf : HasCompactMulSupport f
K : Set α
hK1 : IsCompact K
hK2 : ∀ (x : α), ¬x ∈ K → f x = 1
S : ℝ
hS : S > 0
hS' : ∀ (x : α), x ∈ K → ‖x‖ ≤ S
⊢ ∃ R, 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 1
refine' ⟨S + 1, by positivity, fun x hx => hK2 x ((mt <| hS' x) _)⟩
case intro.intro.intro.intro
𝓕 : Type ?u.1239473
𝕜 : Type ?u.1239476
α : Type u_2
ι : Type ?u.1239482
κ : Type ?u.1239485
E : Type u_1
F : Type ?u.1239491
G : Type ?u.1239494
inst✝¹ : NormedAddGroup α
f : α → E
inst✝ : One E
hf : HasCompactMulSupport f
K : Set α
hK1 : IsCompact K
hK2 : ∀ (x : α), ¬x ∈ K → f x = 1
S : ℝ
hS : S > 0
hS' : ∀ (x : α), x ∈ K → ‖x‖ ≤ S
x : α
hx : ‖x‖ ≤ S
⊢ ‖x‖ < S + 1
case intro.intro.intro.intro
𝓕 : Type ?u.1239473
𝕜 : Type ?u.1239476
α : Type u_2
ι : Type ?u.1239482
κ : Type ?u.1239485
E : Type u_1
F : Type ?u.1239491
G : Type ?u.1239494
inst✝¹ : NormedAddGroup α
f : α → E
inst✝ : One E
hf : HasCompactMulSupport f
K : Set α
hK1 : IsCompact K
hK2 : ∀ (x : α), ¬x ∈ K → f x = 1
S : ℝ
hS : S > 0
hS' : ∀ (x : α), x ∈ K → ‖x‖ ≤ S
x : α
hx : S + 1 ≤ ‖x‖
⊢ ¬‖x‖ ≤ S
contrapose! hx
no goals
case intro.intro.intro.intro
𝓕 : Type ?u.1239473
𝕜 : Type ?u.1239476
α : Type u_2
ι : Type ?u.1239482
κ : Type ?u.1239485
E : Type u_1
F : Type ?u.1239491
G : Type ?u.1239494
inst✝¹ : NormedAddGroup α
f : α → E
inst✝ : One E
hf : HasCompactMulSupport f
K : Set α
hK1 : IsCompact K
hK2 : ∀ (x : α), ¬x ∈ K → f x = 1
S : ℝ
hS : S > 0
hS' : ∀ (x : α), x ∈ K → ‖x‖ ≤ S
x : α
hx : ‖x‖ ≤ S
⊢ ‖x‖ < S + 1
exact lt_add_of_le_of_pos hx zero_lt_one
no goals
𝓕 : Type ?u.1239473
𝕜 : Type ?u.1239476
α : Type u_2
ι : Type ?u.1239482
κ : Type ?u.1239485
E : Type u_1
F : Type ?u.1239491
G : Type ?u.1239494
inst✝¹ : NormedAddGroup α
f : α → E
inst✝ : One E
hf : HasCompactMulSupport f
K : Set α
hK1 : IsCompact K
hK2 : ∀ (x : α), ¬x ∈ K → f x = 1
S : ℝ
hS : S > 0
hS' : ∀ (x : α), x ∈ K → ‖x‖ ≤ S
⊢ 0 < S + 1
positivity