lemmas and structs

Stream: new members

[Iocta]

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

[Iocta]

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

[Kevin Buzzard]

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.