no goals
α : Type u_2
β : Type u_1
γ : Type ?u.850036
δ : Type ?u.850039
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
c : ℝ≥0∞
h₁ : c ≠ 0
h₂ : c ≠ ⊤
⊢ c⁻¹ ≠ 0
simpa using h₂
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.850036
δ : Type ?u.850039
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
c : ℝ≥0∞
h₁ : c ≠ 0
h₂ : c ≠ ⊤
⊢ c⁻¹ ≠ ⊤
simpa using h₁