no goals
α : Type u_1
β : Type ?u.126091
R : Type ?u.126094
R' : Type ?u.126097
ms : Set (OuterMeasure α)
m : OuterMeasure α
s : Set α
h : s = ∅
⊢ ↑⊤ s = ⨅ (_ : s = ∅), 0
simp [h]
no goals
α : Type u_1
β : Type ?u.126091
R : Type ?u.126094
R' : Type ?u.126097
ms : Set (OuterMeasure α)
m : OuterMeasure α
s : Set α
h : Set.Nonempty s
⊢ ↑⊤ s = ⨅ (_ : s = ∅), 0
simp [h, h.ne_empty]