case h
α : Type u_1
β : Type ?u.49288
γ : Type ?u.49291
δ : Type ?u.49294
δ' : Type ?u.49297
ι : Sort uι
s t u : Set α
inst✝ : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ ∀ (x : Bool), MeasurableSet (f ⁻¹' {x})
α : Type u_1
β : Type ?u.49288
γ : Type ?u.49291
δ : Type ?u.49294
δ' : Type ?u.49297
ι : Sort uι
s t u : Set α
inst✝ : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ Measurable f
apply measurable_to_countable'
case h.false
α : Type u_1
β : Type ?u.49288
γ : Type ?u.49291
δ : Type ?u.49294
δ' : Type ?u.49297
ι : Sort uι
s t u : Set α
inst✝ : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ MeasurableSet (f ⁻¹' {false})

case h.true
α : Type u_1
β : Type ?u.49288
γ : Type ?u.49291
δ : Type ?u.49294
δ' : Type ?u.49297
ι : Sort uι
s t u : Set α
inst✝ : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ MeasurableSet (f ⁻¹' {true})
case h
α : Type u_1
β : Type ?u.49288
γ : Type ?u.49291
δ : Type ?u.49294
δ' : Type ?u.49297
ι : Sort uι
s t u : Set α
inst✝ : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ ∀ (x : Bool), MeasurableSet (f ⁻¹' {x})
rintro (- | -)
no goals
case h.true
α : Type u_1
β : Type ?u.49288
γ : Type ?u.49291
δ : Type ?u.49294
δ' : Type ?u.49297
ι : Sort uι
s t u : Set α
inst✝ : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ MeasurableSet (f ⁻¹' {true})
exact h
case h.e'_3
α : Type u_1
β : Type ?u.49288
γ : Type ?u.49291
δ : Type ?u.49294
δ' : Type ?u.49297
ι : Sort uι
s t u : Set α
inst✝ : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ f ⁻¹' {false} = (f ⁻¹' {true})ᶜ
case h.false
α : Type u_1
β : Type ?u.49288
γ : Type ?u.49291
δ : Type ?u.49294
δ' : Type ?u.49297
ι : Sort uι
s t u : Set α
inst✝ : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ MeasurableSet (f ⁻¹' {false})
convert h.compl
no goals
case h.e'_3
α : Type u_1
β : Type ?u.49288
γ : Type ?u.49291
δ : Type ?u.49294
δ' : Type ?u.49297
ι : Sort uι
s t u : Set α
inst✝ : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ f ⁻¹' {false} = (f ⁻¹' {true})ᶜ
rw [← preimage_compl, Bool.compl_singleton, Bool.not_true]