Zulip Chat Archive

Stream: Is there code for X?

Topic: Set of subsets of `t` is equivalent to `set t`

Violeta Hernández (May 29 2022 at 18:35):

Do we have the following equivalence? If so, is there an easy way to prove it?

def equiv.set_of_subset_equiv_set {α : Type u} (t : set α) : {s : set α // s ⊆ t} ≃ set t :=
sorry

Violeta Hernández (May 29 2022 at 18:37):

We can prove {s : set α // s ⊆ t} ≃ Π (a : α), {h : Prop // h → t a} by using subtype_pi_equiv_pi, but I don't know how to finish from here

Yaël Dillies (May 29 2022 at 18:38):

Let me have a go.

Violeta Hernández (May 29 2022 at 18:53):

Here's a direct equivalence, by the way

def equiv.set_of_subset_equiv_set {α : Type u} (t : set α) : {s : set α // s ⊆ t} ≃ set t :=
{ to_fun := λ x, {s : t | s.1 ∈ x.1},
  inv_fun := λ x, ⟨subtype.val '' x, by simp⟩,
  left_inv := λ s, begin
    ext,
    refine ⟨_, λ h, ⟨⟨x, s.2 h⟩, h, rfl⟩⟩,
    rintro ⟨y, hy, rfl⟩,
    exact hy
  end,
  right_inv := λ s, by simp }

Yaël Dillies (May 29 2022 at 18:55):

This is for my cardinal cofinality question, I presume?

import data.set.basic

open set

def subset_equiv_set_coe {α : Type*} (s : set α) : {t : set α // t ⊆ s} ≃ set s :=
{ to_fun := λ t, {x | ↑x ∈ t.1},
  inv_fun := λ t, ⟨t.image subtype.val, image_subset_iff.2 $ λ x _, x.2⟩,
  left_inv := λ t, by { ext, simpa using (λ hx, t.2 hx : x ∈ ↑t → x ∈ s) },
  right_inv := λ t, by simp }