subset of subset

Stream: Is there code for X?

[Heather Macbeth]

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]

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

[Adam Topaz]

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]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Heather Macbeth]

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

[Adam Topaz]

Oh nice.

[Adam Topaz]

import data.set.basic

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

[Adam Topaz]

That image_preimage_coe is a simp lemma :)

[Patrick Massot]

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

[Adam Topaz]

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