α : Type u
m : OuterMeasure α
s s₁ s₂ : Set α
h₁ : IsCaratheodory m s₁
h₂ : IsCaratheodory m s₂
⊢ IsCaratheodory m (s₁ᶜ ∪ s₂ᶜ)
α : Type u
m : OuterMeasure α
s s₁ s₂ : Set α
h₁ : IsCaratheodory m s₁
h₂ : IsCaratheodory m s₂
⊢ IsCaratheodory m (s₁ ∩ s₂)
rw [← isCaratheodory_compl_iff, Set.compl_inter]
no goals
α : Type u
m : OuterMeasure α
s s₁ s₂ : Set α
h₁ : IsCaratheodory m s₁
h₂ : IsCaratheodory m s₂
⊢ IsCaratheodory m (s₁ᶜ ∪ s₂ᶜ)
exact isCaratheodory_union _ (isCaratheodory_compl _ h₁) (isCaratheodory_compl _ h₂)