Stream: Is there code for X?

Topic: subset of subset

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


Adam Topaz (Jan 18 2021 at 21:43):

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

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


Heather Macbeth (Jan 18 2021 at 21:48):

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

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.

Adam Topaz (Jan 18 2021 at 21:49):

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

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.

Oh nice.

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 _ _


Adam Topaz (Jan 18 2021 at 21:52):

That image_preimage_coe is a simp lemma :)

Patrick Massot (Jan 18 2021 at 21:53):

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

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