α : Type u_2
β : Type u_1
γ : Type ?u.280281
ι : Type ?u.280284
inst✝⁴ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
n : ℕ
⊢ ↑↑μ (support ↑((fun n => FinStronglyMeasurable.approx hf n ⊓ FinStronglyMeasurable.approx hg n) n)) < ⊤
α : Type u_2
β : Type u_1
γ : Type ?u.280281
ι : Type ?u.280284
inst✝⁴ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
⊢ FinStronglyMeasurable (f ⊓ g) μ
refine'
  ⟨fun n => hf.approx n ⊓ hg.approx n, fun n => _, fun x =>
    (hf.tendsto_approx x).inf_right_nhds (hg.tendsto_approx x)⟩
α : Type u_2
β : Type u_1
γ : Type ?u.280281
ι : Type ?u.280284
inst✝⁴ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
n : ℕ
⊢ ↑↑μ
      ((support fun x => ↑(FinStronglyMeasurable.approx hf n) x) ∪
        support fun x => ↑(FinStronglyMeasurable.approx hg n) x) <
    ⊤
α : Type u_2
β : Type u_1
γ : Type ?u.280281
ι : Type ?u.280284
inst✝⁴ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
n : ℕ
⊢ ↑↑μ (support ↑((fun n => FinStronglyMeasurable.approx hf n ⊓ FinStronglyMeasurable.approx hg n) n)) < ⊤
refine' (measure_mono (support_inf _ _)).trans_lt _
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.280281
ι : Type ?u.280284
inst✝⁴ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
n : ℕ
⊢ ↑↑μ
      ((support fun x => ↑(FinStronglyMeasurable.approx hf n) x) ∪
        support fun x => ↑(FinStronglyMeasurable.approx hg n) x) <
    ⊤
exact measure_union_lt_top_iff.mpr ⟨hf.fin_support_approx n, hg.fin_support_approx n⟩