case inl
α : Type u_1
m : Set (OuterMeasure α)
h : Set.Nonempty m
⊢ (⨆ (_ : Set.Nonempty ∅), sInfGen m ∅) = ⨅ (μ : OuterMeasure α) (_ : μ ∈ m), ↑μ ∅

case inr
α : Type u_1
m : Set (OuterMeasure α)
h : Set.Nonempty m
t : Set α
ht : Set.Nonempty t
⊢ (⨆ (_ : Set.Nonempty t), sInfGen m t) = ⨅ (μ : OuterMeasure α) (_ : μ ∈ m), ↑μ t
α : Type u_1
m : Set (OuterMeasure α)
h : Set.Nonempty m
t : Set α
⊢ (⨆ (_ : Set.Nonempty t), sInfGen m t) = ⨅ (μ : OuterMeasure α) (_ : μ ∈ m), ↑μ t
rcases t.eq_empty_or_nonempty with (rfl | ht)
case inl.intro
α : Type u_1
m : Set (OuterMeasure α)
μ : OuterMeasure α
hμ : μ ∈ m
⊢ (⨆ (_ : Set.Nonempty ∅), sInfGen m ∅) = ⨅ (μ : OuterMeasure α) (_ : μ ∈ m), ↑μ ∅
case inl
α : Type u_1
m : Set (OuterMeasure α)
h : Set.Nonempty m
⊢ (⨆ (_ : Set.Nonempty ∅), sInfGen m ∅) = ⨅ (μ : OuterMeasure α) (_ : μ ∈ m), ↑μ ∅
rcases h with ⟨μ, hμ⟩
case inl.intro
α : Type u_1
m : Set (OuterMeasure α)
μ : OuterMeasure α
hμ : μ ∈ m
⊢ (⨅ (μ : OuterMeasure α) (_ : μ ∈ m), ↑μ ∅) = ⊥
case inl.intro
α : Type u_1
m : Set (OuterMeasure α)
μ : OuterMeasure α
hμ : μ ∈ m
⊢ (⨆ (_ : Set.Nonempty ∅), sInfGen m ∅) = ⨅ (μ : OuterMeasure α) (_ : μ ∈ m), ↑μ ∅
rw [eq_false Set.not_nonempty_empty, iSup_false, eq_comm]
case inl.intro
α : Type u_1
m : Set (OuterMeasure α)
μ : OuterMeasure α
hμ : μ ∈ m
⊢ (⨅ (μ : OuterMeasure α) (_ : μ ∈ m), 0) = ⊥
case inl.intro
α : Type u_1
m : Set (OuterMeasure α)
μ : OuterMeasure α
hμ : μ ∈ m
⊢ (⨅ (μ : OuterMeasure α) (_ : μ ∈ m), ↑μ ∅) = ⊥
simp_rw [empty']
case inl.intro.h
α : Type u_1
m : Set (OuterMeasure α)
μ : OuterMeasure α
hμ : μ ∈ m
⊢ (⨅ (μ : OuterMeasure α) (_ : μ ∈ m), 0) ≤ ⊥
case inl.intro
α : Type u_1
m : Set (OuterMeasure α)
μ : OuterMeasure α
hμ : μ ∈ m
⊢ (⨅ (μ : OuterMeasure α) (_ : μ ∈ m), 0) = ⊥
apply bot_unique
no goals
case inl.intro.h
α : Type u_1
m : Set (OuterMeasure α)
μ : OuterMeasure α
hμ : μ ∈ m
⊢ (⨅ (μ : OuterMeasure α) (_ : μ ∈ m), 0) ≤ ⊥
refine' iInf_le_of_le μ (iInf_le _ hμ)
no goals
case inr
α : Type u_1
m : Set (OuterMeasure α)
h : Set.Nonempty m
t : Set α
ht : Set.Nonempty t
⊢ (⨆ (_ : Set.Nonempty t), sInfGen m t) = ⨅ (μ : OuterMeasure α) (_ : μ ∈ m), ↑μ t
simp [ht, sInfGen_def]