Coercion on sets of sets

Stream: new members

[Peter Hansen]

I was trying to prove some simple results about the generators of the Borel sets on ℝ.
Things very going pretty well until I got stuck showing the following:

import Mathlib.Tactic

open Set

notation "paving" a => Set (Set a)

def Open_Interval (I : Set ℝ) : Prop := ∃ (a b : ℝ), I = {x | a < x ∧ x < b}

def Open_Interval_R : paving ℝ := {I | Open_Interval I}

def Open_Interval_q (I : Set ℝ) : Prop := ∃ (a b : ℚ), I = {x | a < x ∧ x < b}

def Open_Interval_Q : paving ℚ := {I | Open_Interval_q I}

example : ↑(univ : Set ℚ) ⊆ (univ : Set ℝ) := by simp

example : ↑Open_Interval_Q ⊆ Open_Interval_R := sorry

I know that Lean is build around types and not sets, but I thought the coercion would take care of things. What do I do?

[Eric Wieser]

What do you want the coercion from Set ℚ to Set ℝ to mean?

[Eric Wieser]

Because the answer to your question is currently "write that explicitly"

[Kyle Miller]

One way to write that explicitly is (↑) '' (univ : Set ℚ) for the image under the coercion function

[Peter Hansen]

Eric Wieser said:

What do you want the coercion from Set ℚ to Set ℝ to mean?

I had not really thought about that. Intuitively, it just seemed to make sense. But I guess with sets being propositions on types, it perhaps doesn't.

Kyle Miller said:

One way to write that explicitly is (↑) '' (univ : Set ℚ) for the image under the coercion function

Thanks :) That sort of worked. Though I suspect my whole approach is a bit flawed.

[Peter Hansen]

I think I solved my issue

import Mathlib.Tactic

open Set

notation "paving" a => Set (Set a)

def Open_Interval (I : Set ℝ) : Prop := ∃ (a b : ℝ), I = {x | a < x ∧ x < b}

def Open_Interval_R : paving ℝ := {I | Open_Interval I}

def Open_Interval_q (I : Set ℝ) : Prop := ∃ (a b : ℚ), I = {x | ↑a < x ∧ x < ↑b}

def Open_Interval_Q : paving ℝ := {I | Open_Interval_q I}

example : Open_Interval_Q ⊆ Open_Interval_R := by
  intro x H
  rcases H with ⟨a, b, g⟩
  use a, b
  exact g

What I actually wanted was just the interval with rational end points, which doesn't cause any issues. Thank pushing me in the right direction.