case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) = ∑' (i : ℕ), m (f i) (_ : P (f i))
msU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) ≤ ∑' (i : ℕ), m (f i) (_ : P (f i))
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
⊢ ↑(inducedOuterMeasure m P0 m0) s ≤ ⨅ (t : Set α) (ht : P t) (_ : s ⊆ t), m t ht

case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) = ∑' (i : ℕ), m (f i) (_ : P (f i))
msU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) ≤ ∑' (i : ℕ), m (f i) (_ : P (f i))
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
⊢ (⨅ (t : Set α) (ht : P t) (_ : s ⊆ t), m t ht) ≤ ↑(inducedOuterMeasure m P0 m0) s
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) = ∑' (i : ℕ), m (f i) (_ : P (f i))
msU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) ≤ ∑' (i : ℕ), m (f i) (_ : P (f i))
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
⊢ ↑(inducedOuterMeasure m P0 m0) s = ⨅ (t : Set α) (ht : P t) (_ : s ⊆ t), m t ht
apply le_antisymm
case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) = ∑' (i : ℕ), m (f i) (_ : P (f i))
msU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) ≤ ∑' (i : ℕ), m (f i) (_ : P (f i))
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
⊢ ∀ (i : Set α) (i_1 : P i), s ⊆ i → ↑(inducedOuterMeasure m P0 m0) s ≤ m i i_1
case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) = ∑' (i : ℕ), m (f i) (_ : P (f i))
msU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) ≤ ∑' (i : ℕ), m (f i) (_ : P (f i))
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
⊢ ↑(inducedOuterMeasure m P0 m0) s ≤ ⨅ (t : Set α) (ht : P t) (_ : s ⊆ t), m t ht
simp only [le_iInf_iff]
case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) = ∑' (i : ℕ), m (f i) (_ : P (f i))
msU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) ≤ ∑' (i : ℕ), m (f i) (_ : P (f i))
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s t : Set α
ht : P t
hs : s ⊆ t
⊢ ↑(inducedOuterMeasure m P0 m0) s ≤ m t ht
case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) = ∑' (i : ℕ), m (f i) (_ : P (f i))
msU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) ≤ ∑' (i : ℕ), m (f i) (_ : P (f i))
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
⊢ ∀ (i : Set α) (i_1 : P i), s ⊆ i → ↑(inducedOuterMeasure m P0 m0) s ≤ m i i_1
intro t ht hs
case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) = ∑' (i : ℕ), m (f i) (_ : P (f i))
msU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) ≤ ∑' (i : ℕ), m (f i) (_ : P (f i))
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s t : Set α
ht : P t
hs : s ⊆ t
⊢ ↑(inducedOuterMeasure m P0 m0) t ≤ m t ht
case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) = ∑' (i : ℕ), m (f i) (_ : P (f i))
msU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) ≤ ∑' (i : ℕ), m (f i) (_ : P (f i))
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s t : Set α
ht : P t
hs : s ⊆ t
⊢ ↑(inducedOuterMeasure m P0 m0) s ≤ m t ht
refine' le_trans (mono' _ hs) _
no goals
case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) = ∑' (i : ℕ), m (f i) (_ : P (f i))
msU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) ≤ ∑' (i : ℕ), m (f i) (_ : P (f i))
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s t : Set α
ht : P t
hs : s ⊆ t
⊢ ↑(inducedOuterMeasure m P0 m0) t ≤ m t ht
exact le_of_eq (inducedOuterMeasure_eq' _ msU m_mono _)
case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) = ∑' (i : ℕ), m (f i) (_ : P (f i))
msU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) ≤ ∑' (i : ℕ), m (f i) (_ : P (f i))
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
⊢ ∀ (i : ℕ → Set α),
    (⨅ (t : Set α) (ht : P t) (_ : s ⊆ t), m t ht) ≤ ⨅ (_ : s ⊆ ⋃ (i_1 : ℕ), i i_1), ∑' (i_1 : ℕ), extend m (i i_1)
case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) = ∑' (i : ℕ), m (f i) (_ : P (f i))
msU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) ≤ ∑' (i : ℕ), m (f i) (_ : P (f i))
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
⊢ (⨅ (t : Set α) (ht : P t) (_ : s ⊆ t), m t ht) ≤ ↑(inducedOuterMeasure m P0 m0) s
refine' le_iInf _
case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) = ∑' (i : ℕ), m (f i) (_ : P (f i))
msU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) ≤ ∑' (i : ℕ), m (f i) (_ : P (f i))
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
f : ℕ → Set α
⊢ (⨅ (t : Set α) (ht : P t) (_ : s ⊆ t), m t ht) ≤ ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), extend m (f i)
case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) = ∑' (i : ℕ), m (f i) (_ : P (f i))
msU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) ≤ ∑' (i : ℕ), m (f i) (_ : P (f i))
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
⊢ ∀ (i : ℕ → Set α),
    (⨅ (t : Set α) (ht : P t) (_ : s ⊆ t), m t ht) ≤ ⨅ (_ : s ⊆ ⋃ (i_1 : ℕ), i i_1), ∑' (i_1 : ℕ), extend m (i i_1)
intro f
case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) = ∑' (i : ℕ), m (f i) (_ : P (f i))
msU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) ≤ ∑' (i : ℕ), m (f i) (_ : P (f i))
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
f : ℕ → Set α
⊢ (s ⊆ ⋃ (i : ℕ), f i) → (⨅ (t : Set α) (ht : P t) (_ : s ⊆ t), m t ht) ≤ ∑' (i : ℕ), extend m (f i)
case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) = ∑' (i : ℕ), m (f i) (_ : P (f i))
msU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) ≤ ∑' (i : ℕ), m (f i) (_ : P (f i))
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
f : ℕ → Set α
⊢ (⨅ (t : Set α) (ht : P t) (_ : s ⊆ t), m t ht) ≤ ⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), extend m (f i)
refine' le_iInf _
case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) = ∑' (i : ℕ), m (f i) (_ : P (f i))
msU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) ≤ ∑' (i : ℕ), m (f i) (_ : P (f i))
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
f : ℕ → Set α
hf : s ⊆ ⋃ (i : ℕ), f i
⊢ (⨅ (t : Set α) (ht : P t) (_ : s ⊆ t), m t ht) ≤ ∑' (i : ℕ), extend m (f i)
case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) = ∑' (i : ℕ), m (f i) (_ : P (f i))
msU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) ≤ ∑' (i : ℕ), m (f i) (_ : P (f i))
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
f : ℕ → Set α
⊢ (s ⊆ ⋃ (i : ℕ), f i) → (⨅ (t : Set α) (ht : P t) (_ : s ⊆ t), m t ht) ≤ ∑' (i : ℕ), extend m (f i)
intro hf
case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) = ∑' (i : ℕ), m (f i) (_ : P (f i))
msU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) ≤ ∑' (i : ℕ), m (f i) (_ : P (f i))
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
f : ℕ → Set α
hf : s ⊆ ⋃ (i : ℕ), f i
⊢ (⨅ (t : Set α) (ht : P t) (_ : s ⊆ t), m t ht) ≤ extend m (⋃ (i : ℕ), f i)
case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) = ∑' (i : ℕ), m (f i) (_ : P (f i))
msU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) ≤ ∑' (i : ℕ), m (f i) (_ : P (f i))
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
f : ℕ → Set α
hf : s ⊆ ⋃ (i : ℕ), f i
⊢ (⨅ (t : Set α) (ht : P t) (_ : s ⊆ t), m t ht) ≤ ∑' (i : ℕ), extend m (f i)
refine' le_trans _ (extend_iUnion_le_tsum_nat' _ msU _)
case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) = ∑' (i : ℕ), m (f i) (_ : P (f i))
msU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) ≤ ∑' (i : ℕ), m (f i) (_ : P (f i))
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
f : ℕ → Set α
hf : s ⊆ ⋃ (i : ℕ), f i
⊢ ∀ (i : (fun s => P s) (⋃ (i : ℕ), f i)), (⨅ (t : Set α) (ht : P t) (_ : s ⊆ t), m t ht) ≤ m (⋃ (i : ℕ), f i) i
case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) = ∑' (i : ℕ), m (f i) (_ : P (f i))
msU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) ≤ ∑' (i : ℕ), m (f i) (_ : P (f i))
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
f : ℕ → Set α
hf : s ⊆ ⋃ (i : ℕ), f i
⊢ (⨅ (t : Set α) (ht : P t) (_ : s ⊆ t), m t ht) ≤ extend m (⋃ (i : ℕ), f i)
refine' le_iInf _
case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) = ∑' (i : ℕ), m (f i) (_ : P (f i))
msU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) ≤ ∑' (i : ℕ), m (f i) (_ : P (f i))
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
f : ℕ → Set α
hf : s ⊆ ⋃ (i : ℕ), f i
h2f : (fun s => P s) (⋃ (i : ℕ), f i)
⊢ (⨅ (t : Set α) (ht : P t) (_ : s ⊆ t), m t ht) ≤ m (⋃ (i : ℕ), f i) h2f
case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) = ∑' (i : ℕ), m (f i) (_ : P (f i))
msU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) ≤ ∑' (i : ℕ), m (f i) (_ : P (f i))
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
f : ℕ → Set α
hf : s ⊆ ⋃ (i : ℕ), f i
⊢ ∀ (i : (fun s => P s) (⋃ (i : ℕ), f i)), (⨅ (t : Set α) (ht : P t) (_ : s ⊆ t), m t ht) ≤ m (⋃ (i : ℕ), f i) i
intro h2f
no goals
case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) = ∑' (i : ℕ), m (f i) (_ : P (f i))
msU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
    m (⋃ (i : ℕ), f i) (_ : P (⋃ (i : ℕ), f i)) ≤ ∑' (i : ℕ), m (f i) (_ : P (f i))
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
f : ℕ → Set α
hf : s ⊆ ⋃ (i : ℕ), f i
h2f : (fun s => P s) (⋃ (i : ℕ), f i)
⊢ (⨅ (t : Set α) (ht : P t) (_ : s ⊆ t), m t ht) ≤ m (⋃ (i : ℕ), f i) h2f
refine' iInf_le_of_le _ (iInf_le_of_le h2f <| iInf_le _ hf)