Source indexedlemma · leanprover/lean4:v4.32.0

ENNReal.finsetSum_biSup

Carleson.ToMathlib.Data.ENNReal · Carleson/ToMathlib/Data/ENNReal.lean:59 to 67

Mathematical statement

Exact Lean statement

lemma finsetSum_biSup {f : α → ι → ℝ≥0∞}
    (hf : ∀ i ∈ s, ∀ j ∈ s, ∃ k ∈ s, ∀ a, f a i ≤ f a k ∧ f a j ≤ f a k) :
    ∑ a ∈ t, ⨆ i ∈ s, f a i = ⨆ i ∈ s, ∑ a ∈ t, f a i

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma finsetSum_biSup {f : α → ι → ℝ≥0∞}    (hf : ∀ i ∈ s, ∀ j ∈ s, ∃ k ∈ s, ∀ a, f a i ≤ f a k ∧ f a j ≤ f a k) :    ∑ a ∈ t, ⨆ i ∈ s, f a i = ⨆ i ∈ s, ∑ a ∈ t, f a i := by  induction t using Finset.cons_induction with  | empty => simp  | cons a t ha ihs =>    simp_rw [Finset.sum_cons, ihs]    exact biSup_add_biSup fun i hi j hj ↦ (hf i hi j hj).imp fun k hk ↦      ⟨hk.1, add_le_add (hk.2 a).1 (Finset.sum_le_sum fun i a ↦ (hk.2 _).2)⟩