case basic
α : Type u_1
β : Type ?u.16280
γ : Type ?u.16283
δ : Type ?u.16286
δ' : Type ?u.16289
ι : Sort ?u.16292
s✝ t u : Set α
p : Set α → Prop
C : Set (Set α)
hC : ∀ (t : Set α), t ∈ C → p t
h_empty : p ∅
h_compl : ∀ (t : Set α), p t → p (tᶜ)
h_Union : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n)) → p (⋃ (i : ℕ), f i)
s u✝ : Set α
a✝ : u✝ ∈ C
⊢ p u✝

case empty
α : Type u_1
β : Type ?u.16280
γ : Type ?u.16283
δ : Type ?u.16286
δ' : Type ?u.16289
ι : Sort ?u.16292
s✝ t u : Set α
p : Set α → Prop
C : Set (Set α)
hC : ∀ (t : Set α), t ∈ C → p t
h_empty : p ∅
h_compl : ∀ (t : Set α), p t → p (tᶜ)
h_Union : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n)) → p (⋃ (i : ℕ), f i)
s : Set α
⊢ p ∅

case compl
α : Type u_1
β : Type ?u.16280
γ : Type ?u.16283
δ : Type ?u.16286
δ' : Type ?u.16289
ι : Sort ?u.16292
s✝ t u : Set α
p : Set α → Prop
C : Set (Set α)
hC : ∀ (t : Set α), t ∈ C → p t
h_empty : p ∅
h_compl : ∀ (t : Set α), p t → p (tᶜ)
h_Union : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n)) → p (⋃ (i : ℕ), f i)
s t✝ : Set α
a✝ : GenerateMeasurable C t✝
a_ih✝ : p t✝
⊢ p (t✝ᶜ)

case iUnion
α : Type u_1
β : Type ?u.16280
γ : Type ?u.16283
δ : Type ?u.16286
δ' : Type ?u.16289
ι : Sort ?u.16292
s✝ t u : Set α
p : Set α → Prop
C : Set (Set α)
hC : ∀ (t : Set α), t ∈ C → p t
h_empty : p ∅
h_compl : ∀ (t : Set α), p t → p (tᶜ)
h_Union : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n)) → p (⋃ (i : ℕ), f i)
s : Set α
f✝ : ℕ → Set α
a✝ : ∀ (n : ℕ), GenerateMeasurable C (f✝ n)
a_ih✝ : ∀ (n : ℕ), p (f✝ n)
⊢ p (⋃ (i : ℕ), f✝ i)
α : Type u_1
β : Type ?u.16280
γ : Type ?u.16283
δ : Type ?u.16286
δ' : Type ?u.16289
ι : Sort ?u.16292
s✝ t u : Set α
p : Set α → Prop
C : Set (Set α)
hC : ∀ (t : Set α), t ∈ C → p t
h_empty : p ∅
h_compl : ∀ (t : Set α), p t → p (tᶜ)
h_Union : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n)) → p (⋃ (i : ℕ), f i)
s : Set α
hs : MeasurableSet s
⊢ p s
induction hs
no goals
case basic
α : Type u_1
β : Type ?u.16280
γ : Type ?u.16283
δ : Type ?u.16286
δ' : Type ?u.16289
ι : Sort ?u.16292
s✝ t u : Set α
p : Set α → Prop
C : Set (Set α)
hC : ∀ (t : Set α), t ∈ C → p t
h_empty : p ∅
h_compl : ∀ (t : Set α), p t → p (tᶜ)
h_Union : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n)) → p (⋃ (i : ℕ), f i)
s u✝ : Set α
a✝ : u✝ ∈ C
⊢ p u✝

case empty
α : Type u_1
β : Type ?u.16280
γ : Type ?u.16283
δ : Type ?u.16286
δ' : Type ?u.16289
ι : Sort ?u.16292
s✝ t u : Set α
p : Set α → Prop
C : Set (Set α)
hC : ∀ (t : Set α), t ∈ C → p t
h_empty : p ∅
h_compl : ∀ (t : Set α), p t → p (tᶜ)
h_Union : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n)) → p (⋃ (i : ℕ), f i)
s : Set α
⊢ p ∅

case compl
α : Type u_1
β : Type ?u.16280
γ : Type ?u.16283
δ : Type ?u.16286
δ' : Type ?u.16289
ι : Sort ?u.16292
s✝ t u : Set α
p : Set α → Prop
C : Set (Set α)
hC : ∀ (t : Set α), t ∈ C → p t
h_empty : p ∅
h_compl : ∀ (t : Set α), p t → p (tᶜ)
h_Union : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n)) → p (⋃ (i : ℕ), f i)
s t✝ : Set α
a✝ : GenerateMeasurable C t✝
a_ih✝ : p t✝
⊢ p (t✝ᶜ)

case iUnion
α : Type u_1
β : Type ?u.16280
γ : Type ?u.16283
δ : Type ?u.16286
δ' : Type ?u.16289
ι : Sort ?u.16292
s✝ t u : Set α
p : Set α → Prop
C : Set (Set α)
hC : ∀ (t : Set α), t ∈ C → p t
h_empty : p ∅
h_compl : ∀ (t : Set α), p t → p (tᶜ)
h_Union : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n)) → p (⋃ (i : ℕ), f i)
s : Set α
f✝ : ℕ → Set α
a✝ : ∀ (n : ℕ), GenerateMeasurable C (f✝ n)
a_ih✝ : ∀ (n : ℕ), p (f✝ n)
⊢ p (⋃ (i : ℕ), f✝ i)
exacts [hC _ ‹_›, h_empty, h_compl _ ‹_›, h_Union ‹_› ‹_›]