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 : α // x ∈ filter (fun (x : α) => (f x).Dom) s }) => (f ↑x).get ⋯) (filter (fun (x : α) => (f x).Dom) s).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