Source indexedlemma · leanprover/lean4:v4.32.0

dens₁_mono

Carleson.TileStructure · Carleson/TileStructure.lean:348 to 362

Mathematical statement

Exact Lean statement

lemma dens₁_mono {𝔓₁ 𝔓₂ : Set (𝔓 X)} (h : 𝔓₁ ⊆ 𝔓₂) :
    dens₁ 𝔓₁ ≤ dens₁ 𝔓₂

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma dens₁_mono {𝔓₁ 𝔓₂ : Set (𝔓 X)} (h : 𝔓₁ ⊆ 𝔓₂) :    dens₁ 𝔓₁ ≤ dens₁ 𝔓₂ := by  simp only [dens₁, iSup_le_iff]  intro p hp r hr  apply le_iSup₂_of_le p (h hp) <| ENNReal.mul_le_of_le_div' ?_  simp only [iSup_le_iff]  intro q hq hqr  rw [ENNReal.le_div_iff_mul_le (by left; simp)]  · refine le_iSup₂_of_le r hr ?_    rw [mul_comm]    gcongr    exact le_iSup₂_of_le q (lowerCubes_mono h hq) (le_iSup_iff.mpr fun b a ↦ a hqr)  · left    have hr0 : r ≠ 0 := by positivity    simp [hr0]