How to prove (Set.univ : Set (Fin 2)) = Ω (MeasureTheory)

Stream: new members

[Arshak Parsa]

Is this the right way to make a measurable space?

import Mathlib.Data.Real.Basic
import Mathlib.MeasureTheory.MeasurableSpace.Basic

open MeasureTheory

def σ_algebra : Set (Set (Fin 2)) := {{},{0},{1},{0,1}}

def Ω : Set (Fin 2) := {0,1}

lemma h_empty : ∅ ∈ σ_algebra := by
  tauto

lemma h_compl (s : Set (Fin 2)) : s ∈ σ_algebra → sᶜ ∈ σ_algebra := by
  rw [σ_algebra]
  simp only [Fin.isValue, Set.mem_insert_iff, Set.mem_singleton_iff]
  intro h
  cases h with
    |inl h1 =>
    rw [h1]
    simp
    right
    sorry
    |inr h1 =>
    sorry

def ms : MeasurableSpace (Fin 2) := {
  MeasurableSet' := σ_algebra
  measurableSet_empty := h_empty
  measurableSet_compl := h_compl
  measurableSet_iUnion := sorry
}

Does anyone have any idea how to prove this :

import Mathlib.Data.Real.Basic

def Ω : Set (Fin 2) := {0,1}

lemma lem1 : (Set.univ : Set (Fin 2))  = Ω := by
  rw [Ω]
  sorry

I'm just trying to make a measure space to understand how it works but I'm stuck. :sweat_smile:
Any help is appreciated.

[Alex J. Best]

Fin 2 is already a measurable space according to mathlib (via docs#Fin.instMeasurableSpace), try

#synth MeasurableSpace (Fin 2)

to find this for yourself.

Here is a brute force way to prove your last goal

import Mathlib.Data.Real.Basic
import Mathlib.MeasureTheory.MeasurableSpace.Basic
import Mathlib

def Ω : Set (Fin 2) := {0,1}

lemma lem1 : (Set.univ : Set (Fin 2))  = Ω := by
  rw [Ω]
  ext x
  fin_cases x <;>
  simp

[Alex J. Best]

If you want to define your own measurablespace structure by hand it should work file roughly the way you are doing it. But just wanted to make sure you knew one already exists

[Arshak Parsa]

Now I have a new problem on sets.
When I define a set1 as a type of (Set N), lean assumes the universal set is the set of all natural numbers.
So if I write :

def set1 : (Set ℕ) := {2,3,11}

#check set1ᶜ -- which is  ℕ - {2,3,11}

Well, I want the universal set to be {2,3,11} for set2={2}, and its complement to be {3,11}.
Is there any way to do this ?

I tried something weird but I'm stuck right now :
(by the way, in this code I couldn't assign {2} to set2 so I tried {} instead and fin_cases didn't work in this case
so I think it's not the right way to do this)

def set2 : (Set set1) := {} -- I can't write {2}

example : set2ᶜ = (set1 : Type) := by
  rw [set2 , set1]
  simp
  sorry
  done

[Ruben Van de Velde]

import Mathlib

def set1 : Set ℕ := {2,3,11}

def set2 : Set set1 := { ⟨2, by simp [set1]⟩ }

example : set2ᶜ = { ⟨3, by simp [set1]⟩, ⟨11, by simp [set1]⟩ } := by
  simp [set2]
  ext ⟨x, hx⟩
  simp [set1] at hx
  simp
  constructor
  · exact hx.resolve_left
  · rintro (rfl|rfl) <;> norm_num

[Ruben Van de Velde]

Note in particular that an element of set1 seen as a Type is a pair (x : ℕ, hx : x ∈ set1)