Documentation

Mathlib.Data.Finset.PImage

Image of a Finset α under a partially defined function #

In this file we define Part.toFinset and Finset.pimage. We also prove some trivial lemmas about these definitions.

Tags #

finite set, image, partial function

def Part.toFinset {α : Type u_1} (o : Part α) [Decidable o.Dom] :

Convert an o : Part α with decidable Part.Dom o to Finset α.

Equations
  • o.toFinset = o.toOption.toFinset
Instances For
    @[simp]
    theorem Part.mem_toFinset {α : Type u_1} {o : Part α} [Decidable o.Dom] {x : α} :
    x o.toFinset x o
    @[simp]
    theorem Part.toFinset_none {α : Type u_1} [Decidable Part.none.Dom] :
    Part.none.toFinset =
    @[simp]
    theorem Part.toFinset_some {α : Type u_1} {a : α} [Decidable (Part.some a).Dom] :
    (Part.some a).toFinset = {a}
    @[simp]
    theorem Part.coe_toFinset {α : Type u_1} (o : Part α) [Decidable o.Dom] :
    o.toFinset = {x : α | x o}
    def Finset.pimage {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α →. β) [(x : α) → Decidable (f x).Dom] (s : Finset α) :

    Image of s : Finset α under a partially defined function f : α →. β.

    Equations
    Instances For
      @[simp]
      theorem Finset.mem_pimage {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α →. β} [(x : α) → Decidable (f x).Dom] {s : Finset α} {b : β} :
      b Finset.pimage f s as, b f a
      @[simp]
      theorem Finset.coe_pimage {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α →. β} [(x : α) → Decidable (f x).Dom] {s : Finset α} :
      (Finset.pimage f s) = f.image s
      @[simp]
      theorem Finset.pimage_some {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (f : αβ) [(x : α) → Decidable (Part.some (f x)).Dom] :
      Finset.pimage (fun (x : α) => Part.some (f x)) s = Finset.image f s
      theorem Finset.pimage_congr {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α →. β} {g : α →. β} [(x : α) → Decidable (f x).Dom] [(x : α) → Decidable (g x).Dom] {s : Finset α} {t : Finset α} (h₁ : s = t) (h₂ : xt, f x = g x) :
      theorem Finset.pimage_eq_image_filter {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α →. β} [(x : α) → Decidable (f x).Dom] {s : Finset α} :
      Finset.pimage f s = Finset.image (fun (x : { x : α // x Finset.filter (fun (x : α) => (f x).Dom) s }) => (f x).get ) (Finset.filter (fun (x : α) => (f x).Dom) s).attach

      Rewrite s.pimage f in terms of Finset.filter, Finset.attach, and Finset.image.

      theorem Finset.pimage_union {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α →. β} [(x : α) → Decidable (f x).Dom] {s : Finset α} {t : Finset α} [DecidableEq α] :
      @[simp]
      theorem Finset.pimage_empty {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α →. β} [(x : α) → Decidable (f x).Dom] :
      theorem Finset.pimage_subset {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α →. β} [(x : α) → Decidable (f x).Dom] {s : Finset α} {t : Finset β} :
      Finset.pimage f s t xs, yf x, y t
      theorem Finset.pimage_mono {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α →. β} [(x : α) → Decidable (f x).Dom] {s : Finset α} {t : Finset α} (h : s t) :
      theorem Finset.pimage_inter {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α →. β} [(x : α) → Decidable (f x).Dom] {s : Finset α} {t : Finset α} [DecidableEq α] :