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

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

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

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

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

    Equations
    Instances For
      source
      @[simp]
      theorem Finset.mem_pimage {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α →. β} [(x : α) → Decidable (f x).Dom] {s : Finset α} {b : β} :
      b ∈ pimage f s ↔ ∃ a ∈ s, b ∈ f a
      source
      @[simp]
      theorem Finset.coe_pimage {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α →. β} [(x : α) → Decidable (f x).Dom] {s : Finset α} :
      ↑(pimage f s) = f.image ↑s
      source
      @[simp]
      theorem Finset.pimage_some {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (f : α → β) [(x : α) → Decidable (Part.some (f x)).Dom] :
      pimage (fun (x : α) => Part.some (f x)) s = image f s
      source
      theorem Finset.pimage_congr {α : Type u_1} {β : Type u_2} [DecidableEq β] {f g : α →. β} [(x : α) → Decidable (f x).Dom] [(x : α) → Decidable (g x).Dom] {s t : Finset α} (h₁ : s = t) (h₂ : ∀ x ∈ t, f x = g x) :
      pimage f s = pimage g t
      source
      theorem Finset.pimage_eq_image_filter {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α →. β} [(x : α) → Decidable (f x).Dom] {s : Finset α} :
      pimage f s = image (fun (x : ↥({x ∈ s | (f x).Dom})) => (f ↑x).get ⋯) {x ∈ s | (f x).Dom}.attach

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

      source
      theorem Finset.pimage_union {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α →. β} [(x : α) → Decidable (f x).Dom] {s t : Finset α} [DecidableEq α] :
      pimage f (s ∪ t) = pimage f s ∪ pimage f t
      source
      @[simp]
      theorem Finset.pimage_empty {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α →. β} [(x : α) → Decidable (f x).Dom] :
      pimage f ∅ = ∅
      source
      theorem Finset.pimage_subset {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α →. β} [(x : α) → Decidable (f x).Dom] {s : Finset α} {t : Finset β} :
      pimage f s ⊆ t ↔ ∀ x ∈ s, ∀ y ∈ f x, y ∈ t
      source
      theorem Finset.pimage_mono {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α →. β} [(x : α) → Decidable (f x).Dom] {s t : Finset α} (h : s ⊆ t) :
      pimage f s ⊆ pimage f t
      source
      theorem Finset.pimage_inter {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α →. β} [(x : α) → Decidable (f x).Dom] {s t : Finset α} [DecidableEq α] :
      pimage f (s ∩ t) ⊆ pimage f s ∩ pimage f t