Zulip Chat Archive

Stream: Is there code for X?

Topic: subset of subset


view this post on Zulip Heather Macbeth (Jan 18 2021 at 21:28):

I have two sets u v, with u ⊆ v.

  • Is there a definition/notation for the set of ↥v consisting of elements of u? I came up with (u ∘ coe : set v) but this seems like a hack (it exploits the defequality of set E and E → Prop).
  • If so, is there API for it, such as this lemma saying that when it's coerced from a set in ↥v to a set in the original type, one gets back u?
import data.set.basic

example {E : Type*} {u v : set E} (huv : u  v) :
  coe '' (u  coe : set v) = u :=
begin
  ext y,
  split,
  { rintros y, hy, rfl⟩,
    exact hy },
  { intros hy,
    exact ⟨⟨y, huv hy⟩, hy, rfl }
end

view this post on Zulip Adam Topaz (Jan 18 2021 at 21:43):

This is coe \inv ' U where (coe : V \to E)

view this post on Zulip Adam Topaz (Jan 18 2021 at 21:45):

import tactic
import data.set.basic

example {E : Type*} {u v : set E} (huv : u  v) :
  coe '' ((coe : v  E) ⁻¹' u) = u := by tidy

view this post on Zulip Heather Macbeth (Jan 18 2021 at 21:48):

OK, yes, and tidy works for the version I stated too.

view this post on Zulip Adam Topaz (Jan 18 2021 at 21:49):

In general, I guess tidy can prove that coe '' ((coe : v → E) ⁻¹' u) = u \cap v without the huv assumption.

view this post on Zulip Adam Topaz (Jan 18 2021 at 21:49):

But maybe that's also a lemma somewhere...

view this post on Zulip Heather Macbeth (Jan 18 2021 at 21:49):

Actually, writing as (coe ⁻¹' u : set v) rather than my hack (u ∘ coe : set v) has the advantage that it makes simp [huv] work.

view this post on Zulip Adam Topaz (Jan 18 2021 at 21:50):

Oh nice.

view this post on Zulip Adam Topaz (Jan 18 2021 at 21:52):

import data.set.basic

example {E : Type*} {u v : set E} : coe '' (coe ⁻¹' u : set v) = u  v := subtype.image_preimage_coe _ _

view this post on Zulip Adam Topaz (Jan 18 2021 at 21:52):

That image_preimage_coe is a simp lemma :)

view this post on Zulip Patrick Massot (Jan 18 2021 at 21:53):

I think I wrote that lemma. It looks a lot like things I needed for topology.

view this post on Zulip Adam Topaz (Jan 18 2021 at 21:54):

Yeah this sounds like what one would use to restrict a topology to a subset


Last updated: May 17 2021 at 15:13 UTC