Zulip Chat Archive

Stream: new members

Topic: lemmas and structs


view this post on Zulip Iocta (Mar 08 2021 at 07:22):

What is the relationship between measurable_space.measurable_set_compl and measurable_set.compl? https://github.com/leanprover-community/mathlib/blob/16ef29135dfe41fba018ef7005909c279bee45f5/src/measure_theory/measurable_space.lean#L78-L98

view this post on Zulip Iocta (Mar 08 2021 at 07:29):

e.g. why can't I use this comment instead of the code it follows?

import measure_theory.measure_space
import measure_theory.measurable_space

open measure_theory measure_theory.measure_space classical set

noncomputable theory

variable Ω   : Type
variable [measurable_space Ω]


example [encodable I] (f : I  set Ω) (h :  i : I, measurable_set (f i)) : measurable_set ( i, f i) :=
begin
  apply measurable_set.compl_iff.1,
  rw compl_Inter,
  apply measurable_set.Union, -- apply ‹measurable_space Ω›.measurable_set_Union,
  intro i,
  apply measurable_set.compl_iff.2,
  exact h i,
end

view this post on Zulip Kevin Buzzard (Mar 08 2021 at 08:27):

I don't know this part of the library at all but it seems to me that the answer to why the commented apply doesn't work is simply that the two functions are different, the one that works wants a function from an encodable set (which you have) and the one that doesn't work wants a function from nat (which you don't have). you say "e.g." but it seems to me that this question is different from the question in your first post, the answer to which is probably just that the rephrasing makes it possible to use dot notation because it puts it in the measurable_set namespace so now if hs is a proof that s is measurable then hs.compl is a proof that its complement is measurable. See for example the proof of measurable_set.Inter.


Last updated: May 15 2021 at 23:13 UTC