Preimage of defined subset of \R

Stream: Is there code for X?

[Alex Kontorovich]

Hello, can someone please help me get this to typecheck? Thanks!

import measure_theory.measure.measure_space

noncomputable theory

open measure_theory measurable_space

def pm_one_space : set ℝ := {-1, 1}

universe u
variables {Ω : Type u} [measurable_space Ω] [measurable_space ↥pm_one_space]

lemma meas_pm (Z : Ω → pm_one_space) (h : measurable Z) :
measurable_set (Z ⁻¹' {(1:ℝ)}) :=
begin
  sorry
end

[Alex J. Best]

You need to take the 1 in pm_one_space, by showing 1 is a mem of this space

import measure_theory.measure.measure_space

noncomputable theory

open measure_theory measurable_space

def pm_one_space : set ℝ := {-1, 1}

universe u
variables {Ω : Type u} [measurable_space Ω] [measurable_space ↥pm_one_space]

lemma meas_pm (Z : Ω → pm_one_space) (h : measurable Z) :
measurable_set (Z ⁻¹' {⟨(1:ℝ), by simp [pm_one_space]⟩}) :=
begin
  sorry
end

[Eric Wieser]

You might find that ℤˣ is more convenient than your pm_one_space; for one, it comes with a group structure

[Alex Kontorovich]

It makes some things much nicer, thanks! But now I'm stuck on this??

import measure_theory.measure.measure_space

noncomputable theory

open measure_theory measurable_space

universe u
variables {Ω : Type u} [measurable_space Ω]

lemma meas_pm (Z : Ω → ℤˣ) :
{ω : Ω | (Z ω : ℝ) = 1} = (Z ⁻¹' {1}) :=
begin
  ext x,
  simp only [coe_coe, set.mem_set_of_eq, set.mem_preimage, set.mem_singleton_iff],
  norm_cast,
  sorry
end

[Kevin Buzzard]

simp finishes it for me

[Kevin Buzzard]

and squeeze_simp tells me that exact units.coe_eq_one, works too.

[Alex Kontorovich]

Argh! Thanks. I'd tried simp at first (that's the leading simp only), then norm_cast; for some reason assumed simp wouldn't finish it if it hadn't already.

[Kevin Buzzard]

The thing about the cast lemmas is that you sometimes want to push the coercions inwards and sometimes outwards. It's not clear which is simpler out of \u(1+x) and 1+\u(x), so it's not clear whether a lemma saying they're equal should be a simp lemma or not. We have norm_cast pushing one way and push_cast pushing the other way, and these tactics know lemmas which simp doesn't (and apply them in different directions). This means that simp and the cast lemmas can solve a different set of goals.