Mapping from subtype of finsets to finset of subtypes

Stream: new members

[Jihoon Hyun]

Given some p, how can I make a natural mapping from {S : Finset (Finset α) // ∀ s ∈ S, p s} to Finset {s : Finset α // p s}?

[Daniel Weber]

You can deconstruct it, then use docs#Finset.attach to get s = Finset {x : Finset a // x in s}, and then use docs#Finset.map with docs#Subtype.impEmbedding with the property of s

[Yakov Pechersky]

(deleted)

[Jihoon Hyun]

import Mathlib.Data.Finset.Basic
import Mathlib.Data.Finset.Image
import Mathlib.Logic.Embedding.Basic

section Finset

open Finset Function Subtype

def Finset.Subtype.Equiv {α : Type*} {p : Finset α → Prop} :
    Equiv {S : Finset (Finset α) // ∀ s ∈ S, p s} (Finset {s : Finset α // p s}) where
  toFun S := S.val.attach.map (impEmbedding _ _ S.property)
  invFun S := ⟨S.map ⟨fun s ↦ s.val, Subtype.val_injective⟩, fun s h ↦
    have ⟨v, _, h⟩ := Embedding.coeFn_mk _ _ ▸ mem_map.mp h
    h ▸ v.property⟩
  left_inv S := by
    ext s; constructor <;> intro h <;>
    simp only [mem_map, mem_attach, true_and, Subtype.exists, Embedding.coeFn_mk,
      exists_and_right, exists_eq_right, impEmbedding, Subtype.mk.injEq] at *
    · rcases h with ⟨_, _, h₁, h₂⟩; exact h₂ ▸ h₁
    · use S.property _ h, s
  right_inv S := by
    ext s; constructor <;> intro h <;>
    simp only [mem_map, mem_attach, true_and, Subtype.exists, Embedding.coeFn_mk,
      exists_and_right, exists_eq_right, impEmbedding, Subtype.mk.injEq] at *
    · rcases h with ⟨_, ⟨_, h₁⟩, h₂⟩; exact h₂ ▸ h₁
    · use s, ⟨s.property, h⟩

end Finset

section Set

def Set.Subtype.Equiv {α : Type*} {p : Set α → Prop} :
    Equiv {S : Set (Set α) // ∀ s ∈ S, p s} (Set {s : Set α // p s}) where
  toFun S s := S.val s
  invFun S := ⟨fun s ↦ ∃ h : p s, S ⟨s, h⟩, fun _ h ↦ h.1⟩
  left_inv S := by ext; exact ⟨fun h ↦ h.2, fun h ↦ ⟨S.property _ h, h⟩⟩
  right_inv S := by ext s; exact ⟨fun h ↦ h.2, fun h ↦ ⟨s.property, h⟩⟩

end Set

I guess these instances can be placed somewhere in mathlib. Where would be the best place for these? .Basic file of each types?

[Daniel Weber]

docs#Equiv

[Daniel Weber]

It isn't a typeclass - I'm not sure why instance accepts this, it might be a bug

[Jihoon Hyun]

Thanks for the reply again! It probably isn't a bug if I'm right, but I should definitely get rid of that. Also as it's not a typeclass then I'll just place them somewhere in basic files for each types.

[Jihoon Hyun]

#19514