α : Type u_1
β : Type u_2
γ : Type ?u.22535
δ : Type ?u.22538
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
this : {a | r a (↑f a)} = ⋃ (b : β) (_ : b ∈ range ↑f), {a | r a b} ∩ ↑f ⁻¹' {b}
⊢ MeasurableSet {a | r a (↑f a)}
α : Type u_1
β : Type u_2
γ : Type ?u.22535
δ : Type ?u.22538
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
⊢ MeasurableSet {a | r a (↑f a)}
have : { a | r a (f a) } = ⋃ b ∈ range f, { a | r a b } ∩ f ⁻¹' {b} := by
  ext a
  suffices r a (f a) ↔ ∃ i, r a (f i) ∧ f a = f i by simpa
  exact ⟨fun h => ⟨a, ⟨h, rfl⟩⟩, fun ⟨a', ⟨h', e⟩⟩ => e.symm ▸ h'⟩
α : Type u_1
β : Type u_2
γ : Type ?u.22535
δ : Type ?u.22538
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
this : {a | r a (↑f a)} = ⋃ (b : β) (_ : b ∈ range ↑f), {a | r a b} ∩ ↑f ⁻¹' {b}
⊢ MeasurableSet (⋃ (b : β) (_ : b ∈ range ↑f), {a | r a b} ∩ ↑f ⁻¹' {b})
α : Type u_1
β : Type u_2
γ : Type ?u.22535
δ : Type ?u.22538
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
this : {a | r a (↑f a)} = ⋃ (b : β) (_ : b ∈ range ↑f), {a | r a b} ∩ ↑f ⁻¹' {b}
⊢ MeasurableSet {a | r a (↑f a)}
rw [this]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.22535
δ : Type ?u.22538
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
this : {a | r a (↑f a)} = ⋃ (b : β) (_ : b ∈ range ↑f), {a | r a b} ∩ ↑f ⁻¹' {b}
⊢ MeasurableSet (⋃ (b : β) (_ : b ∈ range ↑f), {a | r a b} ∩ ↑f ⁻¹' {b})
exact
  MeasurableSet.biUnion f.finite_range.countable fun b _ =>
    MeasurableSet.inter (h b) (f.measurableSet_fiber _)
case h
α : Type u_1
β : Type u_2
γ : Type ?u.22535
δ : Type ?u.22538
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
a : α
⊢ a ∈ {a | r a (↑f a)} ↔ a ∈ ⋃ (b : β) (_ : b ∈ range ↑f), {a | r a b} ∩ ↑f ⁻¹' {b}
α : Type u_1
β : Type u_2
γ : Type ?u.22535
δ : Type ?u.22538
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
⊢ {a | r a (↑f a)} = ⋃ (b : β) (_ : b ∈ range ↑f), {a | r a b} ∩ ↑f ⁻¹' {b}
ext a
case h
α : Type u_1
β : Type u_2
γ : Type ?u.22535
δ : Type ?u.22538
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
a : α
⊢ r a (↑f a) ↔ ∃ i, r a (↑f i) ∧ ↑f a = ↑f i
case h
α : Type u_1
β : Type u_2
γ : Type ?u.22535
δ : Type ?u.22538
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
a : α
⊢ a ∈ {a | r a (↑f a)} ↔ a ∈ ⋃ (b : β) (_ : b ∈ range ↑f), {a | r a b} ∩ ↑f ⁻¹' {b}
suffices r a (f a) ↔ ∃ i, r a (f i) ∧ f a = f i by simpa
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.22535
δ : Type ?u.22538
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
a : α
⊢ r a (↑f a) ↔ ∃ i, r a (↑f i) ∧ ↑f a = ↑f i
exact ⟨fun h => ⟨a, ⟨h, rfl⟩⟩, fun ⟨a', ⟨h', e⟩⟩ => e.symm ▸ h'⟩
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.22535
δ : Type ?u.22538
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
a : α
this : r a (↑f a) ↔ ∃ i, r a (↑f i) ∧ ↑f a = ↑f i
⊢ a ∈ {a | r a (↑f a)} ↔ a ∈ ⋃ (b : β) (_ : b ∈ range ↑f), {a | r a b} ∩ ↑f ⁻¹' {b}
simpa