case intro
α : Type u_2
β : Type u_1
γ : Type ?u.1004756
δ : Type ?u.1004759
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
val✝ : Encodable β
⊢ (∫⁻ (a : α), ⨆ (b : β), f b a ∂μ) = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
α : Type u_2
β : Type u_1
γ : Type ?u.1004756
δ : Type ?u.1004759
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
⊢ (∫⁻ (a : α), ⨆ (b : β), f b a ∂μ) = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
cases nonempty_encodable β
case intro.inl
α : Type u_2
β : Type u_1
γ : Type ?u.1004756
δ : Type ?u.1004759
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
val✝ : Encodable β
h✝ : IsEmpty β
⊢ (∫⁻ (a : α), ⨆ (b : β), f b a ∂μ) = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ

case intro.inr
α : Type u_2
β : Type u_1
γ : Type ?u.1004756
δ : Type ?u.1004759
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
val✝ : Encodable β
h✝ : Nonempty β
⊢ (∫⁻ (a : α), ⨆ (b : β), f b a ∂μ) = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
case intro
α : Type u_2
β : Type u_1
γ : Type ?u.1004756
δ : Type ?u.1004759
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
val✝ : Encodable β
⊢ (∫⁻ (a : α), ⨆ (b : β), f b a ∂μ) = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
cases isEmpty_or_nonempty β
case intro.inr
α : Type u_2
β : Type u_1
γ : Type ?u.1004756
δ : Type ?u.1004759
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
⊢ (∫⁻ (a : α), ⨆ (b : β), f b a ∂μ) = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
case intro.inr
α : Type u_2
β : Type u_1
γ : Type ?u.1004756
δ : Type ?u.1004759
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
val✝ : Encodable β
h✝ : Nonempty β
⊢ (∫⁻ (a : α), ⨆ (b : β), f b a ∂μ) = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
inhabit β
case intro.inr
α : Type u_2
β : Type u_1
γ : Type ?u.1004756
δ : Type ?u.1004759
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
this : ∀ (a : α), (⨆ (b : β), f b a) = ⨆ (n : ℕ), f (Directed.sequence f h_directed n) a
⊢ (∫⁻ (a : α), ⨆ (b : β), f b a ∂μ) = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
case intro.inr
α : Type u_2
β : Type u_1
γ : Type ?u.1004756
δ : Type ?u.1004759
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
⊢ (∫⁻ (a : α), ⨆ (b : β), f b a ∂μ) = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
have : ∀ a, (⨆ b, f b a) = ⨆ n, f (h_directed.sequence f n) a := by
  intro a
  refine' le_antisymm (iSup_le fun b => _) (iSup_le fun n => le_iSup (fun n => f n a) _)
  exact le_iSup_of_le (encode b + 1) (h_directed.le_sequence b a)
no goals
case intro.inl
α : Type u_2
β : Type u_1
γ : Type ?u.1004756
δ : Type ?u.1004759
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
val✝ : Encodable β
h✝ : IsEmpty β
⊢ (∫⁻ (a : α), ⨆ (b : β), f b a ∂μ) = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
simp [iSup_of_empty]
α : Type u_2
β : Type u_1
γ : Type ?u.1004756
δ : Type ?u.1004759
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
a : α
⊢ (⨆ (b : β), f b a) = ⨆ (n : ℕ), f (Directed.sequence f h_directed n) a
α : Type u_2
β : Type u_1
γ : Type ?u.1004756
δ : Type ?u.1004759
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
⊢ ∀ (a : α), (⨆ (b : β), f b a) = ⨆ (n : ℕ), f (Directed.sequence f h_directed n) a
intro a
α : Type u_2
β : Type u_1
γ : Type ?u.1004756
δ : Type ?u.1004759
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
a : α
b : β
⊢ f b a ≤ ⨆ (n : ℕ), f (Directed.sequence f h_directed n) a
α : Type u_2
β : Type u_1
γ : Type ?u.1004756
δ : Type ?u.1004759
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
a : α
⊢ (⨆ (b : β), f b a) = ⨆ (n : ℕ), f (Directed.sequence f h_directed n) a
refine' le_antisymm (iSup_le fun b => _) (iSup_le fun n => le_iSup (fun n => f n a) _)
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.1004756
δ : Type ?u.1004759
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
a : α
b : β
⊢ f b a ≤ ⨆ (n : ℕ), f (Directed.sequence f h_directed n) a
exact le_iSup_of_le (encode b + 1) (h_directed.le_sequence b a)
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.1004756
δ : Type ?u.1004759
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
this : ∀ (a : α), (⨆ (b : β), f b a) = ⨆ (n : ℕ), f (Directed.sequence f h_directed n) a
⊢ (∫⁻ (a : α), ⨆ (b : β), f b a ∂μ) = ∫⁻ (a : α), ⨆ (n : ℕ), f (Directed.sequence f h_directed n) a ∂μ
simp only [this]
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.1004756
δ : Type ?u.1004759
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
this : ∀ (a : α), (⨆ (b : β), f b a) = ⨆ (n : ℕ), f (Directed.sequence f h_directed n) a
n : ℕ
⊢ (∫⁻ (a : α), f (Directed.sequence f h_directed n) a ∂μ) ≤ ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ

case refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.1004756
δ : Type ?u.1004759
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
this : ∀ (a : α), (⨆ (b : β), f b a) = ⨆ (n : ℕ), f (Directed.sequence f h_directed n) a
b : β
⊢ (∫⁻ (a : α), f b a ∂μ) ≤ ⨆ (n : ℕ), ∫⁻ (a : α), f (Directed.sequence f h_directed n) a ∂μ
α : Type u_2
β : Type u_1
γ : Type ?u.1004756
δ : Type ?u.1004759
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
this : ∀ (a : α), (⨆ (b : β), f b a) = ⨆ (n : ℕ), f (Directed.sequence f h_directed n) a
⊢ (⨆ (n : ℕ), ∫⁻ (a : α), f (Directed.sequence f h_directed n) a ∂μ) = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
refine' le_antisymm (iSup_le fun n => _) (iSup_le fun b => _)
no goals
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.1004756
δ : Type ?u.1004759
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
this : ∀ (a : α), (⨆ (b : β), f b a) = ⨆ (n : ℕ), f (Directed.sequence f h_directed n) a
n : ℕ
⊢ (∫⁻ (a : α), f (Directed.sequence f h_directed n) a ∂μ) ≤ ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
exact le_iSup (fun b => ∫⁻ a, f b a ∂μ) _
no goals
case refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.1004756
δ : Type ?u.1004759
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
this : ∀ (a : α), (⨆ (b : β), f b a) = ⨆ (n : ℕ), f (Directed.sequence f h_directed n) a
b : β
⊢ (∫⁻ (a : α), f b a ∂μ) ≤ ⨆ (n : ℕ), ∫⁻ (a : α), f (Directed.sequence f h_directed n) a ∂μ
exact le_iSup_of_le (encode b + 1) (lintegral_mono <| h_directed.le_sequence b)