Mathlib.Data.Finset.Defs

Finset structure

(α : Type*)

Full source

/-- `Finset α` is the type of finite sets of elements of `α`. It is implemented
  as a multiset (a list up to permutation) which has no duplicate elements. -/
structure Finset (α : Type*) where
  /-- The underlying multiset -/
  val : Multiset α
  /-- `val` contains no duplicates -/
  nodup : Nodup val

Finite set

Informal description

The structure `Finset α` represents the type of finite subsets of a type `α`. It is implemented as a multiset (a list up to permutation) with no duplicate elements.

Multiset.canLiftFinset instance

{α} : CanLift (Multiset α) (Finset α) Finset.val Multiset.Nodup

Full source

instance Multiset.canLiftFinset {α} : CanLift (Multiset α) (Finset α) Finset.val Multiset.Nodup :=
  ⟨fun m hm => ⟨⟨m, hm⟩, rfl⟩⟩

Lifting Nodup Multisets to Finite Sets

Informal description

For any type $\alpha$, there is a canonical way to lift a multiset $m$ of elements in $\alpha$ to a finite set (finset) provided that $m$ has no duplicate elements (i.e., $m$ is nodup).

Finset.val_injective theorem

: Injective (val : Finset α → Multiset α)

Full source

theorem val_injective : Injective (val : Finset α → Multiset α) := fun _ _ => eq_of_veq

Injectivity of the Underlying Multiset of a Finite Set

Informal description

The function that maps a finite set `s : Finset α` to its underlying multiset `val s` is injective. In other words, for any two finite sets `s` and `t`, if their underlying multisets are equal (`val s = val t`), then the finite sets themselves are equal (`s = t`).

Finset.val_inj theorem

{s t : Finset α} : s.1 = t.1 ↔ s = t

Full source

@[simp]
theorem val_inj {s t : Finset α} : s.1 = t.1 ↔ s = t :=
  val_injective.eq_iff

Equality of Finite Sets via Underlying Multisets

Informal description

For any two finite sets $s$ and $t$ of type $\alpha$, the equality of their underlying multisets $s.1 = t.1$ holds if and only if $s = t$.

Finset.decidableEq instance

[DecidableEq α] : DecidableEq (Finset α)

Full source

instance decidableEq [DecidableEq α] : DecidableEq (Finset α)
  | _, _ => decidable_of_iff _ val_inj

Decidable Equality for Finite Sets

Informal description

For any type $\alpha$ with decidable equality, the type of finite subsets $\text{Finset } \alpha$ also has decidable equality.

Finset.instMembership instance

: Membership α (Finset α)

Full source

instance : Membership α (Finset α) :=
  ⟨fun s a => a ∈ s.1⟩

Membership in Finite Sets

Informal description

For any type $\alpha$, we say $a \in s$ for $a \in \alpha$ and $s$ a finite subset of $\alpha$ if $a$ appears in the underlying multiset of $s$.

Finset.mem_def theorem

{a : α} {s : Finset α} : a ∈ s ↔ a ∈ s.1

Full source

theorem mem_def {a : α} {s : Finset α} : a ∈ sa ∈ s ↔ a ∈ s.1 :=
  Iff.rfl

Membership in Finite Sets via Underlying Multiset

Informal description

For any element $a$ of type $\alpha$ and any finite set $s$ of type $\alpha$, the statement $a \in s$ holds if and only if $a$ is an element of the underlying multiset $s.1$ of $s$.

Finset.mem_val theorem

{a : α} {s : Finset α} : (a ∈ s.1) = (a ∈ s)

Full source

@[simp]
theorem mem_val {a : α} {s : Finset α} : (a ∈ s.1) = (a ∈ s) := rfl

Membership in Finite Set via Underlying Multiset

Informal description

For any element $a$ of type $\alpha$ and any finite set $s$ of type $\alpha$, the statement that $a$ belongs to the underlying multiset of $s$ is equivalent to $a$ belonging to $s$ itself. In other words, $a \in s.1 \leftrightarrow a \in s$.

Finset.mem_mk theorem

{a : α} {s nd} : a ∈ @Finset.mk α s nd ↔ a ∈ s

Full source

@[simp]
theorem mem_mk {a : α} {s nd} : a ∈ @Finset.mk α s nda ∈ @Finset.mk α s nd ↔ a ∈ s :=
  Iff.rfl

Membership in Constructed Finite Set via Underlying Multiset

Informal description

For any element $a$ of type $\alpha$ and any finite set constructed as `Finset.mk s nd` (where `s` is a multiset and `nd` is a proof that `s` has no duplicates), the membership $a \in \text{Finset.mk } s \text{ } nd$ holds if and only if $a \in s$.

Finset.decidableMem instance

[_h : DecidableEq α] (a : α) (s : Finset α) : Decidable (a ∈ s)

Full source

instance decidableMem [_h : DecidableEq α] (a : α) (s : Finset α) : Decidable (a ∈ s) :=
  Multiset.decidableMem _ _

Decidability of Membership in Finite Sets

Informal description

For any type $\alpha$ with decidable equality, given an element $a \in \alpha$ and a finite set $s \subseteq \alpha$, it is decidable whether $a$ is a member of $s$.

Finset.forall_mem_not_eq theorem

{s : Finset α} {a : α} : (∀ b ∈ s, ¬a = b) ↔ a ∉ s

Full source

@[simp] lemma forall_mem_not_eq {s : Finset α} {a : α} : (∀ b ∈ s, ¬ a = b) ↔ a ∉ s := by aesop

Characterization of Non-Membership in Finite Sets via Inequality

Informal description

For any finite set $s$ of type $\alpha$ and any element $a \in \alpha$, the following are equivalent: 1. For all $b \in s$, $a \neq b$. 2. $a \notin s$.

Finset.forall_mem_not_eq' theorem

{s : Finset α} {a : α} : (∀ b ∈ s, ¬b = a) ↔ a ∉ s

Full source

@[simp] lemma forall_mem_not_eq' {s : Finset α} {a : α} : (∀ b ∈ s, ¬ b = a) ↔ a ∉ s := by aesop

Characterization of Non-Membership in Finite Sets via Reverse Inequality

Informal description

For any finite set $s$ of type $\alpha$ and any element $a \in \alpha$, the following are equivalent: 1. For all $b \in s$, $b \neq a$. 2. $a$ is not a member of $s$ ($a \notin s$).

Finset.toSet definition

(s : Finset α) : Set α

Full source

/-- Convert a finset to a set in the natural way. -/
@[coe] def toSet (s : Finset α) : Set α :=
  { a | a ∈ s }

Finite set to set conversion

Informal description

The function maps a finite set $s$ of type $\alpha$ to the corresponding set $\{a \mid a \in s\}$ in the natural way, where $a \in s$ denotes membership in the finite set $s$.

Finset.instCoeTCSet instance

: CoeTC (Finset α) (Set α)

Full source

/-- Convert a finset to a set in the natural way. -/
instance : CoeTC (Finset α) (Set α) :=
  ⟨toSet⟩

Natural Coercion from Finite Sets to Sets

Informal description

Every finite set $s$ of type $\alpha$ can be naturally coerced to a set $\{a \mid a \in s\}$.

Finset.mem_coe theorem

{a : α} {s : Finset α} : a ∈ (s : Set α) ↔ a ∈ (s : Finset α)

Full source

@[simp, norm_cast]
theorem mem_coe {a : α} {s : Finset α} : a ∈ (s : Set α)a ∈ (s : Set α) ↔ a ∈ (s : Finset α) :=
  Iff.rfl

Equivalence of Membership in Finite Set and its Set Coercion

Informal description

For any element $a$ of type $\alpha$ and any finite set $s$ of type $\alpha$, the element $a$ belongs to the set corresponding to $s$ if and only if $a$ belongs to the finite set $s$ itself. In other words, $a \in s$ as a set membership is equivalent to $a \in s$ as a finite set membership.

Finset.setOf_mem theorem

{α} {s : Finset α} : {a | a ∈ s} = s

Full source

@[simp]
theorem setOf_mem {α} {s : Finset α} : { a | a ∈ s } = s :=
  rfl

Set Comprehension of Finite Set Membership Equals Original Set

Informal description

For any finite set $s$ of type $\alpha$, the set $\{a \mid a \in s\}$ is equal to $s$ itself.

Finset.coe_mem theorem

{s : Finset α} (x : (s : Set α)) : ↑x ∈ s

Full source

@[simp]
theorem coe_mem {s : Finset α} (x : (s : Set α)) : ↑x ∈ s :=
  x.2

Membership in Finite Set via Set Coercion

Informal description

For any finite set $s$ of type $\alpha$ and any element $x$ in the corresponding set $\{a \mid a \in s\}$, the underlying element $x$ belongs to the finite set $s$.

Finset.mk_coe theorem

{s : Finset α} (x : (s : Set α)) {h} : (⟨x, h⟩ : (s : Set α)) = x

Full source

theorem mk_coe {s : Finset α} (x : (s : Set α)) {h} : (⟨x, h⟩ : (s : Set α)) = x :=
  Subtype.coe_eta _ _

Subtype Construction Equals Original Element in Finite Set Coercion

Informal description

For any finite set $s$ of type $\alpha$ and any element $x$ in the set corresponding to $s$, the element $\langle x, h \rangle$ (where $h$ is a proof that $x \in s$) is equal to $x$ when viewed as an element of the set $\{a \mid a \in s\}$.

Finset.decidableMem' instance

[DecidableEq α] (a : α) (s : Finset α) : Decidable (a ∈ (s : Set α))

Full source

instance decidableMem' [DecidableEq α] (a : α) (s : Finset α) : Decidable (a ∈ (s : Set α)) :=
  s.decidableMem _

Decidability of Membership in Finite Sets via Set Coercion

Informal description

For any type $\alpha$ with decidable equality, given an element $a \in \alpha$ and a finite set $s \subseteq \alpha$, it is decidable whether $a$ is a member of the set corresponding to $s$.

Finset.ext theorem

{s₁ s₂ : Finset α} (h : ∀ a, a ∈ s₁ ↔ a ∈ s₂) : s₁ = s₂

Full source

@[ext]
theorem ext {s₁ s₂ : Finset α} (h : ∀ a, a ∈ s₁a ∈ s₁ ↔ a ∈ s₂) : s₁ = s₂ :=
  (val_inj.symm.trans <| s₁.nodup.ext s₂.nodup).mpr h

Extensionality of Finite Sets

Informal description

For any two finite sets $s_1$ and $s_2$ of type $\alpha$, if for every element $a \in \alpha$ we have $a \in s_1$ if and only if $a \in s_2$, then $s_1 = s_2$.

Finset.coe_inj theorem

{s₁ s₂ : Finset α} : (s₁ : Set α) = s₂ ↔ s₁ = s₂

Full source

@[simp, norm_cast]
theorem coe_inj {s₁ s₂ : Finset α} : (s₁ : Set α) = s₂ ↔ s₁ = s₂ :=
  Set.ext_iff.trans Finset.ext_iff.symm

Equality of Finite Sets via Set Coercion

Informal description

For any two finite sets $s_1$ and $s_2$ of type $\alpha$, the corresponding sets (via coercion) are equal if and only if the finite sets themselves are equal, i.e., $(s_1 : \text{Set } \alpha) = s_2 \leftrightarrow s_1 = s_2$.

Finset.coe_injective theorem

{α} : Injective ((↑) : Finset α → Set α)

Full source

theorem coe_injective {α} : Injective ((↑) : Finset α → Set α) := fun _s _t => coe_inj.1

Injectivity of Finite Set to Set Coercion

Informal description

The canonical embedding from the type of finite subsets of $\alpha$ to the type of sets of $\alpha$ is injective. That is, for any two finite sets $s_1, s_2 \subseteq \alpha$, if $s_1$ and $s_2$ are equal as sets, then $s_1 = s_2$ as finite sets.

Finset.instCoeSortType instance

{α : Type u} : CoeSort (Finset α) (Type u)

Full source

/-- Coercion from a finset to the corresponding subtype. -/
instance {α : Type u} : CoeSort (Finset α) (Type u) :=
  ⟨fun s => { x // x ∈ s }⟩

Finite Subsets as Subtypes

Informal description

For any type $\alpha$, a finite subset $s$ of $\alpha$ can be coerced to the type of all elements $x$ that belong to $s$. This means that $s$ can be treated as the subtype $\{x \in \alpha \mid x \in s\}$.

Finset.forall_coe theorem

{α : Type*} (s : Finset α) (p : s → Prop) : (∀ x : s, p x) ↔ ∀ (x : α) (h : x ∈ s), p ⟨x, h⟩

Full source

protected theorem forall_coe {α : Type*} (s : Finset α) (p : s → Prop) :
    (∀ x : s, p x) ↔ ∀ (x : α) (h : x ∈ s), p ⟨x, h⟩ :=
  Subtype.forall

Universal Quantification over Finite Sets via Subtype and Membership

Informal description

For any finite subset $s$ of a type $\alpha$ and any predicate $p$ on elements of $s$, the statement that $p(x)$ holds for all $x \in s$ is equivalent to the statement that for every $x \in \alpha$ such that $x \in s$, the predicate $p$ holds for the element $\langle x, h\rangle$ where $h$ is a proof that $x \in s$.

Finset.exists_coe theorem

{α : Type*} (s : Finset α) (p : s → Prop) : (∃ x : s, p x) ↔ ∃ (x : α) (h : x ∈ s), p ⟨x, h⟩

Full source

protected theorem exists_coe {α : Type*} (s : Finset α) (p : s → Prop) :
    (∃ x : s, p x) ↔ ∃ (x : α) (h : x ∈ s), p ⟨x, h⟩ :=
  Subtype.exists

Existence in Finite Sets via Subtype and Membership

Informal description

For any finite subset $s$ of a type $\alpha$ and any predicate $p$ on elements of $s$, there exists an element $x$ in $s$ satisfying $p(x)$ if and only if there exists an element $x$ in $\alpha$ that belongs to $s$ and satisfies $p(x)$ when viewed as an element of $s$.

Finset.PiFinsetCoe.canLift instance

 (ι : Type*) (α : ι → Type*) [_ne : ∀ i, Nonempty (α i)] (s : Finset ι) :
  CanLift (∀ i : s, α i) (∀ i, α i) (fun f i => f i) fun _ => True

Full source

instance PiFinsetCoe.canLift (ι : Type*) (α : ι → Type*) [_ne : ∀ i, Nonempty (α i)]
    (s : Finset ι) : CanLift (∀ i : s, α i) (∀ i, α i) (fun f i => f i) fun _ => True :=
  PiSubtype.canLift ι α (· ∈ s)

Lifting Functions from Finite Subsets to Full Domain

Informal description

For any type family $\alpha$ indexed by a type $\iota$ where each $\alpha_i$ is nonempty, and any finite subset $s$ of $\iota$, there exists a canonical way to lift functions from the subtype $\{i \in \iota \mid i \in s\}$ to $\alpha$ to functions from all of $\iota$ to $\alpha$ via the inclusion map.

Finset.PiFinsetCoe.canLift' instance

(ι α : Type*) [_ne : Nonempty α] (s : Finset ι) : CanLift (s → α) (ι → α) (fun f i => f i) fun _ => True

Full source

instance PiFinsetCoe.canLift' (ι α : Type*) [_ne : Nonempty α] (s : Finset ι) :
    CanLift (s → α) (ι → α) (fun f i => f i) fun _ => True :=
  PiFinsetCoe.canLift ι (fun _ => α) s

Lifting Functions from Finite Subsets to Full Domain (Constant Codomain Case)

Informal description

For any type $\iota$, a nonempty type $\alpha$, and a finite subset $s$ of $\iota$, there exists a canonical way to lift functions from $s$ to $\alpha$ to functions from all of $\iota$ to $\alpha$ via the inclusion map.

Finset.FinsetCoe.canLift instance

(s : Finset α) : CanLift α s (↑) fun a => a ∈ s

Full source

instance FinsetCoe.canLift (s : Finset α) : CanLift α s (↑) fun a => a ∈ s where
  prf a ha := ⟨⟨a, ha⟩, rfl⟩

Lifting Condition for Finite Sets

Informal description

For any finite subset $s$ of a type $\alpha$, there exists a lifting condition that allows elements of $\alpha$ to be lifted to elements of $s$ via the canonical inclusion map, provided the element is a member of $s$.

Finset.coe_sort_coe theorem

(s : Finset α) : ((s : Set α) : Sort _) = s

Full source

@[simp, norm_cast]
theorem coe_sort_coe (s : Finset α) : ((s : Set α) : Sort _) = s :=
  rfl

Equality of Coerced Finite Set and Original Finite Set

Informal description

For any finite subset $s$ of a type $\alpha$, the type of elements of the set $s$ (obtained by coercing $s$ to a set and then to a sort) is equal to $s$ itself.

Finset.instHasSubset instance

: HasSubset (Finset α)

Full source

instance : HasSubset (Finset α) :=
  ⟨fun s t => ∀ ⦃a⦄, a ∈ s → a ∈ t⟩

Subset Relation on Finite Sets

Informal description

For any type $\alpha$, the finite subsets of $\alpha$ have a subset relation $\subseteq$ defined on them.

Finset.instHasSSubset instance

: HasSSubset (Finset α)

Full source

instance : HasSSubset (Finset α) :=
  ⟨fun s t => s ⊆ t ∧ ¬t ⊆ s⟩

Strict Subset Relation on Finite Sets

Informal description

For any type $\alpha$, the finite subsets of $\alpha$ have a strict subset relation $\subset$ defined on them.

Finset.partialOrder instance

: PartialOrder (Finset α)

Full source

instance partialOrder : PartialOrder (Finset α) where
  le := (· ⊆ ·)
  lt := (· ⊂ ·)
  le_refl _ _ := id
  le_trans _ _ _ hst htu _ ha := htu <| hst ha
  le_antisymm _ _ hst hts := ext fun _ => ⟨@hst _, @hts _⟩

Partial Order on Finite Sets

Informal description

For any type $\alpha$, the finite subsets of $\alpha$ form a partial order under the subset relation $\subseteq$.

Finset.subset_of_le theorem

: s ≤ t → s ⊆ t

Full source

theorem subset_of_le : s ≤ t → s ⊆ t := id

Subset Relation Implication from Partial Order on Finite Sets

Informal description

For any two finite sets $s$ and $t$ of type $\alpha$, if $s$ is less than or equal to $t$ in the partial order of finite sets (i.e., $s \leq t$), then $s$ is a subset of $t$ (i.e., $s \subseteq t$).

Finset.instIsReflSubset instance

: IsRefl (Finset α) (· ⊆ ·)

Full source

instance : IsRefl (Finset α) (· ⊆ ·) :=
  show IsRefl (Finset α) (· ≤ ·) by infer_instance

Reflexivity of Subset Relation on Finite Sets

Informal description

For any type $\alpha$, the subset relation $\subseteq$ on finite subsets of $\alpha$ is reflexive. That is, for any finite set $s \subseteq \alpha$, we have $s \subseteq s$.

Finset.instIsTransSubset instance

: IsTrans (Finset α) (· ⊆ ·)

Full source

instance : IsTrans (Finset α) (· ⊆ ·) :=
  show IsTrans (Finset α) (· ≤ ·) by infer_instance

Transitivity of Subset Relation on Finite Sets

Informal description

For any type $\alpha$, the subset relation $\subseteq$ on finite subsets of $\alpha$ is transitive. That is, for any three finite subsets $s, t, u$ of $\alpha$, if $s \subseteq t$ and $t \subseteq u$, then $s \subseteq u$.

Finset.instIsAntisymmSubset instance

: IsAntisymm (Finset α) (· ⊆ ·)

Full source

instance : IsAntisymm (Finset α) (· ⊆ ·) :=
  show IsAntisymm (Finset α) (· ≤ ·) by infer_instance

Antisymmetry of the Subset Relation on Finite Sets

Informal description

For any type $\alpha$, the subset relation $\subseteq$ on finite subsets of $\alpha$ is antisymmetric. That is, for any two finite subsets $s$ and $t$ of $\alpha$, if $s \subseteq t$ and $t \subseteq s$, then $s = t$.

Finset.instIsIrreflSSubset instance

: IsIrrefl (Finset α) (· ⊂ ·)

Full source

instance : IsIrrefl (Finset α) (· ⊂ ·) :=
  show IsIrrefl (Finset α) (· < ·) by infer_instance

Irreflexivity of Strict Subset Relation on Finite Sets

Informal description

For any type $\alpha$, the strict subset relation $\subset$ on finite subsets of $\alpha$ is irreflexive, meaning that for any finite subset $s \subseteq \alpha$, $s \subset s$ does not hold.

Finset.instIsTransSSubset instance

: IsTrans (Finset α) (· ⊂ ·)

Full source

instance : IsTrans (Finset α) (· ⊂ ·) :=
  show IsTrans (Finset α) (· < ·) by infer_instance

Transitivity of Strict Subset Relation on Finite Sets

Informal description

For any type $\alpha$, the strict subset relation $\subset$ on finite subsets of $\alpha$ is transitive. That is, for any finite sets $s, t, u \subseteq \alpha$, if $s \subset t$ and $t \subset u$, then $s \subset u$.

Finset.instIsAsymmSSubset instance

: IsAsymm (Finset α) (· ⊂ ·)

Full source

instance : IsAsymm (Finset α) (· ⊂ ·) :=
  show IsAsymm (Finset α) (· < ·) by infer_instance

Asymmetry of Strict Subset Relation on Finite Sets

Informal description

For any type $\alpha$, the strict subset relation $\subset$ on finite subsets of $\alpha$ is asymmetric. That is, for any two finite sets $s$ and $t$ of type $\alpha$, if $s \subset t$ then it is not the case that $t \subset s$.

Finset.instIsNonstrictStrictOrderSubsetSSubset instance

: IsNonstrictStrictOrder (Finset α) (· ⊆ ·) (· ⊂ ·)

Full source

instance : IsNonstrictStrictOrder (Finset α) (· ⊆ ·) (· ⊂ ·) :=
  ⟨fun _ _ => Iff.rfl⟩

Subset Relations on Finite Sets Form Nonstrict-Strict Order Pair

Informal description

For any type $\alpha$, the subset relation $\subseteq$ and strict subset relation $\subset$ on finite subsets of $\alpha$ form a nonstrict-strict order pair. That is, for any finite sets $s$ and $t$ of type $\alpha$, we have $s \subset t$ if and only if $s \subseteq t$ and $\neg (t \subseteq s)$.

Finset.subset_def theorem

: s ⊆ t ↔ s.1 ⊆ t.1

Full source

theorem subset_def : s ⊆ ts ⊆ t ↔ s.1 ⊆ t.1 :=
  Iff.rfl

Subset Relation on Finite Sets via Underlying Multisets

Informal description

For any two finite sets $s$ and $t$ of type $\alpha$, the subset relation $s \subseteq t$ holds if and only if the underlying multiset of $s$ is a submultiset of the underlying multiset of $t$.

Finset.ssubset_def theorem

: s ⊂ t ↔ s ⊆ t ∧ ¬t ⊆ s

Full source

theorem ssubset_def : s ⊂ ts ⊂ t ↔ s ⊆ t ∧ ¬t ⊆ s :=
  Iff.rfl

Characterization of Strict Subset Relation for Finite Sets

Informal description

For any two finite sets $s$ and $t$ of type $\alpha$, the strict subset relation $s \subset t$ holds if and only if $s$ is a subset of $t$ and $t$ is not a subset of $s$.

Finset.Subset.refl theorem

(s : Finset α) : s ⊆ s

Full source

theorem Subset.refl (s : Finset α) : s ⊆ s :=
  Multiset.Subset.refl _

Reflexivity of Subset Relation for Finite Sets

Informal description

For any finite set $s$ of type $\alpha$, the subset relation $s \subseteq s$ holds.

Finset.Subset.rfl theorem

{s : Finset α} : s ⊆ s

Full source

protected theorem Subset.rfl {s : Finset α} : s ⊆ s :=
  Subset.refl _

Reflexivity of Subset Relation for Finite Sets

Informal description

For any finite set $s$ of type $\alpha$, the subset relation $s \subseteq s$ holds.

Finset.subset_of_eq theorem

{s t : Finset α} (h : s = t) : s ⊆ t

Full source

protected theorem subset_of_eq {s t : Finset α} (h : s = t) : s ⊆ t :=
  h ▸ Subset.refl _

Subset Relation Holds for Equal Finite Sets

Informal description

For any two finite sets $s$ and $t$ of type $\alpha$, if $s = t$, then $s \subseteq t$.

Finset.Subset.trans theorem

{s₁ s₂ s₃ : Finset α} : s₁ ⊆ s₂ → s₂ ⊆ s₃ → s₁ ⊆ s₃

Full source

theorem Subset.trans {s₁ s₂ s₃ : Finset α} : s₁ ⊆ s₂ → s₂ ⊆ s₃ → s₁ ⊆ s₃ :=
  Multiset.Subset.trans

Transitivity of Subset Relation for Finite Sets

Informal description

For any finite sets $s₁, s₂, s₃$ of type $\alpha$, if $s₁ \subseteq s₂$ and $s₂ \subseteq s₃$, then $s₁ \subseteq s₃$.

Finset.Superset.trans theorem

{s₁ s₂ s₃ : Finset α} : s₁ ⊇ s₂ → s₂ ⊇ s₃ → s₁ ⊇ s₃

Full source

theorem Superset.trans {s₁ s₂ s₃ : Finset α} : s₁ ⊇ s₂ → s₂ ⊇ s₃ → s₁ ⊇ s₃ := fun h' h =>
  Subset.trans h h'

Transitivity of Superset Relation for Finite Sets

Informal description

For any finite sets $s₁, s₂, s₃$ of type $\alpha$, if $s₁ \supseteq s₂$ and $s₂ \supseteq s₃$, then $s₁ \supseteq s₃$.

Finset.mem_of_subset theorem

{s₁ s₂ : Finset α} {a : α} : s₁ ⊆ s₂ → a ∈ s₁ → a ∈ s₂

Full source

theorem mem_of_subset {s₁ s₂ : Finset α} {a : α} : s₁ ⊆ s₂ → a ∈ s₁ → a ∈ s₂ :=
  Multiset.mem_of_subset

Membership Preservation under Subset Inclusion for Finite Sets

Informal description

For any finite sets $s₁$ and $s₂$ of type $\alpha$ and any element $a \in \alpha$, if $s₁$ is a subset of $s₂$ and $a$ belongs to $s₁$, then $a$ also belongs to $s₂$.

Finset.not_mem_mono theorem

{s t : Finset α} (h : s ⊆ t) {a : α} : a ∉ t → a ∉ s

Full source

theorem not_mem_mono {s t : Finset α} (h : s ⊆ t) {a : α} : a ∉ t → a ∉ s :=
  mt <| @h _

Non-membership Preservation under Subset Inclusion for Finite Sets

Informal description

For any finite sets $s$ and $t$ of a type $\alpha$, if $s$ is a subset of $t$ and an element $a \in \alpha$ is not in $t$, then $a$ is also not in $s$.

Finset.Subset.antisymm theorem

{s₁ s₂ : Finset α} (H₁ : s₁ ⊆ s₂) (H₂ : s₂ ⊆ s₁) : s₁ = s₂

Full source

theorem Subset.antisymm {s₁ s₂ : Finset α} (H₁ : s₁ ⊆ s₂) (H₂ : s₂ ⊆ s₁) : s₁ = s₂ :=
  ext fun a => ⟨@H₁ a, @H₂ a⟩

Antisymmetry of Subset Relation for Finite Sets

Informal description

For any two finite sets $s_1$ and $s_2$ of a type $\alpha$, if $s_1$ is a subset of $s_2$ and $s_2$ is a subset of $s_1$, then $s_1 = s_2$.

Finset.subset_iff theorem

{s₁ s₂ : Finset α} : s₁ ⊆ s₂ ↔ ∀ ⦃x⦄, x ∈ s₁ → x ∈ s₂

Full source

theorem subset_iff {s₁ s₂ : Finset α} : s₁ ⊆ s₂s₁ ⊆ s₂ ↔ ∀ ⦃x⦄, x ∈ s₁ → x ∈ s₂ :=
  Iff.rfl

Characterization of Subset Relation for Finite Sets via Membership

Informal description

For any two finite sets $s₁$ and $s₂$ of a type $\alpha$, $s₁$ is a subset of $s₂$ if and only if every element $x$ in $s₁$ is also in $s₂$.

Finset.coe_subset theorem

{s₁ s₂ : Finset α} : (s₁ : Set α) ⊆ s₂ ↔ s₁ ⊆ s₂

Full source

@[simp, norm_cast]
theorem coe_subset {s₁ s₂ : Finset α} : (s₁ : Set α) ⊆ s₂(s₁ : Set α) ⊆ s₂ ↔ s₁ ⊆ s₂ :=
  Iff.rfl

Subset Relation Correspondence Between Finite Sets and Their Set Coercions

Informal description

For any two finite sets $s₁$ and $s₂$ of a type $\alpha$, the set corresponding to $s₁$ is a subset of $s₂$ if and only if $s₁$ is a subset of $s₂$ in the finite set sense.

Finset.val_le_iff theorem

{s₁ s₂ : Finset α} : s₁.1 ≤ s₂.1 ↔ s₁ ⊆ s₂

Full source

@[simp]
theorem val_le_iff {s₁ s₂ : Finset α} : s₁.1 ≤ s₂.1 ↔ s₁ ⊆ s₂ :=
  le_iff_subset s₁.2

Multiset Ordering Characterizes Subset Relation for Finite Sets

Informal description

For any two finite sets $s₁$ and $s₂$ of type $\alpha$, the multiset underlying $s₁$ is less than or equal to the multiset underlying $s₂$ if and only if $s₁$ is a subset of $s₂$.

Finset.Subset.antisymm_iff theorem

{s₁ s₂ : Finset α} : s₁ = s₂ ↔ s₁ ⊆ s₂ ∧ s₂ ⊆ s₁

Full source

theorem Subset.antisymm_iff {s₁ s₂ : Finset α} : s₁ = s₂ ↔ s₁ ⊆ s₂ ∧ s₂ ⊆ s₁ :=
  le_antisymm_iff

Antisymmetry of Subset Relation for Finite Sets: $s₁ = s₂ \leftrightarrow s₁ \subseteq s₂ \land s₂ \subseteq s₁$

Informal description

For any two finite sets $s₁$ and $s₂$ of type $\alpha$, $s₁ = s₂$ if and only if $s₁ \subseteq s₂$ and $s₂ \subseteq s₁$.

Finset.not_subset theorem

: ¬s ⊆ t ↔ ∃ x ∈ s, x ∉ t

Full source

theorem not_subset : ¬s ⊆ t¬s ⊆ t ↔ ∃ x ∈ s, x ∉ t := by simp only [← coe_subset, Set.not_subset, mem_coe]

Characterization of Non-Subset Relation for Finite Sets

Informal description

For any two finite sets $s$ and $t$ of type $\alpha$, the statement that $s$ is not a subset of $t$ is equivalent to the existence of an element $x \in s$ such that $x \notin t$.

Finset.le_eq_subset theorem

: ((· ≤ ·) : Finset α → Finset α → Prop) = (· ⊆ ·)

Full source

@[simp]
theorem le_eq_subset : ((· ≤ ·) : Finset α → Finset α → Prop) = (· ⊆ ·) :=
  rfl

Partial Order on Finite Sets Coincides with Subset Relation

Informal description

For any type $\alpha$, the partial order relation $\leq$ on finite subsets of $\alpha$ is equal to the subset relation $\subseteq$.

Finset.lt_eq_subset theorem

: ((· < ·) : Finset α → Finset α → Prop) = (· ⊂ ·)

Full source

@[simp]
theorem lt_eq_subset : ((· < ·) : Finset α → Finset α → Prop) = (· ⊂ ·) :=
  rfl

Strict Order on Finite Sets Coincides with Strict Subset Relation

Informal description

For any type $\alpha$, the strict partial order relation `<` on finite subsets of $\alpha$ is equal to the strict subset relation $\subset$.

Finset.le_iff_subset theorem

{s₁ s₂ : Finset α} : s₁ ≤ s₂ ↔ s₁ ⊆ s₂

Full source

theorem le_iff_subset {s₁ s₂ : Finset α} : s₁ ≤ s₂ ↔ s₁ ⊆ s₂ :=
  Iff.rfl

Partial Order on Finite Sets Coincides with Subset Relation

Informal description

For any two finite subsets $s_1$ and $s_2$ of a type $\alpha$, the partial order relation $s_1 \leq s_2$ holds if and only if $s_1$ is a subset of $s_2$, i.e., $s_1 \subseteq s_2$.

Finset.lt_iff_ssubset theorem

{s₁ s₂ : Finset α} : s₁ < s₂ ↔ s₁ ⊂ s₂

Full source

theorem lt_iff_ssubset {s₁ s₂ : Finset α} : s₁ < s₂ ↔ s₁ ⊂ s₂ :=
  Iff.rfl

Strict Order on Finite Sets is Equivalent to Strict Subset Relation

Informal description

For any two finite sets $s_1$ and $s_2$ of type $\alpha$, the strict partial order relation $s_1 < s_2$ holds if and only if $s_1$ is a strict subset of $s_2$ (i.e., $s_1 \subset s_2$).

Finset.coe_ssubset theorem

{s₁ s₂ : Finset α} : (s₁ : Set α) ⊂ s₂ ↔ s₁ ⊂ s₂

Full source

@[simp, norm_cast]
theorem coe_ssubset {s₁ s₂ : Finset α} : (s₁ : Set α) ⊂ s₂(s₁ : Set α) ⊂ s₂ ↔ s₁ ⊂ s₂ :=
  show (s₁ : Set α) ⊂ s₂(s₁ : Set α) ⊂ s₂ ↔ s₁ ⊆ s₂ ∧ ¬s₂ ⊆ s₁ by simp only [Set.ssubset_def, Finset.coe_subset]

Equivalence of Strict Subset Relations Between Finite Sets and Their Set Coercions

Informal description

For any two finite sets $s_1$ and $s_2$ of type $\alpha$, the set corresponding to $s_1$ is a strict subset of the set corresponding to $s_2$ if and only if $s_1$ is a strict subset of $s_2$ as finite sets. In symbols: $(s_1 : \text{Set } \alpha) \subset s_2 \leftrightarrow s_1 \subset s_2$.

Finset.val_lt_iff theorem

{s₁ s₂ : Finset α} : s₁.1 < s₂.1 ↔ s₁ ⊂ s₂

Full source

@[simp]
theorem val_lt_iff {s₁ s₂ : Finset α} : s₁.1 < s₂.1 ↔ s₁ ⊂ s₂ :=
  and_congr val_le_iff <| not_congr val_le_iff

Multiset Ordering Characterizes Strict Subset Relation for Finite Sets

Informal description

For any two finite sets $s₁$ and $s₂$ of type $\alpha$, the underlying multiset of $s₁$ is strictly less than the underlying multiset of $s₂$ if and only if $s₁$ is a strict subset of $s₂$.

Finset.val_strictMono theorem

: StrictMono (val : Finset α → Multiset α)

Full source

lemma val_strictMono : StrictMono (val : Finset α → Multiset α) := fun _ _ ↦ val_lt_iff.2

Strict Monotonicity of Finite Set to Multiset Embedding

Informal description

The function that maps a finite set $s : \text{Finset} \alpha$ to its underlying multiset is strictly monotone with respect to the strict subset relation on finite sets and the strict multiset order. That is, for any two finite sets $s_1, s_2 \subseteq \alpha$, if $s_1 \subset s_2$, then the multiset associated with $s_1$ is strictly less than the multiset associated with $s_2$ in the multiset order.

Finset.ssubset_iff_subset_ne theorem

{s t : Finset α} : s ⊂ t ↔ s ⊆ t ∧ s ≠ t

Full source

theorem ssubset_iff_subset_ne {s t : Finset α} : s ⊂ ts ⊂ t ↔ s ⊆ t ∧ s ≠ t :=
  @lt_iff_le_and_ne _ _ s t

Characterization of Strict Subset for Finite Sets: $s \subset t \leftrightarrow s \subseteq t \land s \neq t$

Informal description

For any two finite sets $s$ and $t$ of type $\alpha$, $s$ is a strict subset of $t$ if and only if $s$ is a subset of $t$ and $s$ is not equal to $t$.

Finset.ssubset_iff_of_subset theorem

{s₁ s₂ : Finset α} (h : s₁ ⊆ s₂) : s₁ ⊂ s₂ ↔ ∃ x ∈ s₂, x ∉ s₁

Full source

theorem ssubset_iff_of_subset {s₁ s₂ : Finset α} (h : s₁ ⊆ s₂) : s₁ ⊂ s₂s₁ ⊂ s₂ ↔ ∃ x ∈ s₂, x ∉ s₁ :=
  Set.ssubset_iff_of_subset h

Characterization of Strict Subset for Finite Sets via Non-Member Element

Informal description

For any two finite sets $s_1$ and $s_2$ of elements of type $\alpha$, if $s_1$ is a subset of $s_2$ (i.e., $s_1 \subseteq s_2$), then $s_1$ is a strict subset of $s_2$ (i.e., $s_1 \subset s_2$) if and only if there exists an element $x \in s_2$ such that $x \notin s_1$.

Finset.ssubset_of_ssubset_of_subset theorem

{s₁ s₂ s₃ : Finset α} (hs₁s₂ : s₁ ⊂ s₂) (hs₂s₃ : s₂ ⊆ s₃) : s₁ ⊂ s₃

Full source

theorem ssubset_of_ssubset_of_subset {s₁ s₂ s₃ : Finset α} (hs₁s₂ : s₁ ⊂ s₂) (hs₂s₃ : s₂ ⊆ s₃) :
    s₁ ⊂ s₃ :=
  Set.ssubset_of_ssubset_of_subset hs₁s₂ hs₂s₃

Transitivity of Strict Subset via Subset for Finite Sets

Informal description

For any finite sets $s₁, s₂, s₃$ of elements of type $\alpha$, if $s₁$ is a strict subset of $s₂$ and $s₂$ is a subset of $s₃$, then $s₁$ is a strict subset of $s₃$.

Finset.ssubset_of_subset_of_ssubset theorem

{s₁ s₂ s₃ : Finset α} (hs₁s₂ : s₁ ⊆ s₂) (hs₂s₃ : s₂ ⊂ s₃) : s₁ ⊂ s₃

Full source

theorem ssubset_of_subset_of_ssubset {s₁ s₂ s₃ : Finset α} (hs₁s₂ : s₁ ⊆ s₂) (hs₂s₃ : s₂ ⊂ s₃) :
    s₁ ⊂ s₃ :=
  Set.ssubset_of_subset_of_ssubset hs₁s₂ hs₂s₃

Transitivity of Strict Subset via Subset and Strict Subset for Finite Sets

Informal description

For any finite sets $s_1, s_2, s_3$ of elements of type $\alpha$, if $s_1$ is a subset of $s_2$ and $s_2$ is a strict subset of $s_3$, then $s_1$ is a strict subset of $s_3$.

Finset.exists_of_ssubset theorem

{s₁ s₂ : Finset α} (h : s₁ ⊂ s₂) : ∃ x ∈ s₂, x ∉ s₁

Full source

theorem exists_of_ssubset {s₁ s₂ : Finset α} (h : s₁ ⊂ s₂) : ∃ x ∈ s₂, x ∉ s₁ :=
  Set.exists_of_ssubset h

Existence of Element in Strict Superset of Finite Sets

Informal description

For any finite subsets $s₁$ and $s₂$ of a type $\alpha$, if $s₁$ is a strict subset of $s₂$ (denoted $s₁ \subset s₂$), then there exists an element $x \in s₂$ such that $x \notin s₁$.

Finset.isWellFounded_ssubset instance

: IsWellFounded (Finset α) (· ⊂ ·)

Full source

instance isWellFounded_ssubset : IsWellFounded (Finset α) (· ⊂ ·) :=
  Subrelation.isWellFounded (InvImage _ _) val_lt_iff.2

Well-foundedness of Strict Subset Relation on Finite Sets

Informal description

The strict subset relation $\subset$ on finite subsets of a type $\alpha$ is well-founded. That is, every non-empty collection of finite subsets of $\alpha$ has a minimal element with respect to $\subset$.

Finset.wellFoundedLT instance

: WellFoundedLT (Finset α)

Full source

instance wellFoundedLT : WellFoundedLT (Finset α) :=
  Finset.isWellFounded_ssubset

Well-foundedness of Strict Subset Relation on Finite Sets

Informal description

The strict subset relation $\subset$ on finite subsets of a type $\alpha$ is well-founded.

Finset.coeEmb definition

: Finset α ↪o Set α

Full source

/-- Coercion to `Set α` as an `OrderEmbedding`. -/
def coeEmb : FinsetFinset α ↪o Set α :=
  ⟨⟨(↑), coe_injective⟩, coe_subset⟩

Order embedding from finite sets to sets

Informal description

The order embedding from the type of finite subsets of $\alpha$ to the type of sets of $\alpha$ is given by the canonical inclusion function, which is injective and preserves the subset order. Specifically, for any finite set $s \subseteq \alpha$, the embedding maps $s$ to the corresponding set $\{a \mid a \in s\}$.

Finset.coe_coeEmb theorem

: ⇑(coeEmb : Finset α ↪o Set α) = ((↑) : Finset α → Set α)

Full source

@[simp]
theorem coe_coeEmb : ⇑(coeEmb : FinsetFinset α ↪o Set α) = ((↑) : Finset α → Set α) :=
  rfl

Embedding-coercion equality for finite sets

Informal description

The underlying function of the order embedding `coeEmb` from finite sets to sets is equal to the canonical coercion function from finite sets to sets. That is, for any finite set $s : \text{Finset} \alpha$, we have $\text{coeEmb}(s) = s$ (where $s$ on the right is interpreted as a set).

Finset.decidableDforallFinset instance

{p : ∀ a ∈ s, Prop} [_hp : ∀ (a) (h : a ∈ s), Decidable (p a h)] : Decidable (∀ (a) (h : a ∈ s), p a h)

Full source

instance decidableDforallFinset {p : ∀ a ∈ s, Prop} [_hp : ∀ (a) (h : a ∈ s), Decidable (p a h)] :
    Decidable (∀ (a) (h : a ∈ s), p a h) :=
  Multiset.decidableDforallMultiset

Decidability of Universal Quantification over Finite Sets

Informal description

For any finite set $s$ of type $\alpha$ and a predicate $p$ on elements of $s$ (where $p$ is decidable for each element), the universal quantification $\forall a \in s, p(a)$ is decidable.

Finset.instDecidableRelSubset instance

[DecidableEq α] : DecidableRel (α := Finset α) (· ⊆ ·)

Full source

instance instDecidableRelSubset [DecidableEq α] : DecidableRel (α := Finset α) (· ⊆ ·) :=
  fun _ _ ↦ decidableDforallFinset

Decidability of Subset Relation on Finite Sets

Informal description

For any type $\alpha$ with decidable equality, the subset relation $\subseteq$ on finite subsets of $\alpha$ is decidable.

Finset.instDecidableRelSSubset instance

[DecidableEq α] : DecidableRel (α := Finset α) (· ⊂ ·)

Full source

instance instDecidableRelSSubset [DecidableEq α] : DecidableRel (α := Finset α) (· ⊂ ·) :=
  fun _ _ ↦ instDecidableAnd

Decidability of Strict Subset Relation on Finite Sets

Informal description

For any type $\alpha$ with decidable equality, the strict subset relation $\subset$ on finite subsets of $\alpha$ is decidable.

Finset.instDecidableLE instance

[DecidableEq α] : DecidableLE (Finset α)

Full source

instance instDecidableLE [DecidableEq α] : DecidableLE (Finset α) :=
  instDecidableRelSubset

Decidability of the $\leq$ Relation on Finite Sets

Informal description

For any type $\alpha$ with decidable equality, the relation $\leq$ on finite subsets of $\alpha$ is decidable.

Finset.instDecidableLT instance

[DecidableEq α] : DecidableLT (Finset α)

Full source

instance instDecidableLT [DecidableEq α] : DecidableLT (Finset α) :=
  instDecidableRelSSubset

Decidability of Strict Order on Finite Sets

Informal description

For any type $\alpha$ with decidable equality, the strict order relation $<$ on finite subsets of $\alpha$ is decidable.

Finset.decidableDExistsFinset instance

{p : ∀ a ∈ s, Prop} [_hp : ∀ (a) (h : a ∈ s), Decidable (p a h)] : Decidable (∃ (a : _) (h : a ∈ s), p a h)

Full source

instance decidableDExistsFinset {p : ∀ a ∈ s, Prop} [_hp : ∀ (a) (h : a ∈ s), Decidable (p a h)] :
    Decidable (∃ (a : _) (h : a ∈ s), p a h) :=
  Multiset.decidableDexistsMultiset

Decidability of Existential Quantification over Finite Sets

Informal description

For any finite set $s$ of type $\alpha$ and any predicate $p$ defined for elements $a \in s$ with decidable values, it is decidable whether there exists an element $a \in s$ such that $p(a)$ holds.

Finset.decidableExistsAndFinset instance

{p : α → Prop} [_hp : ∀ (a), Decidable (p a)] : Decidable (∃ a ∈ s, p a)

Full source

instance decidableExistsAndFinset {p : α → Prop} [_hp : ∀ (a), Decidable (p a)] :
    Decidable (∃ a ∈ s, p a) :=
  decidable_of_iff (∃ (a : _) (_ : a ∈ s), p a) (by simp)

Decidability of Existential Quantification over Finite Sets

Informal description

For any finite set $s$ of type $\alpha$ and any predicate $p : \alpha \to \mathrm{Prop}$ with decidable values, it is decidable whether there exists an element $a \in s$ such that $p(a)$ holds.

Finset.decidableExistsAndFinsetCoe instance

{p : α → Prop} [DecidablePred p] : Decidable (∃ a ∈ (s : Set α), p a)

Full source

instance decidableExistsAndFinsetCoe {p : α → Prop} [DecidablePred p] :
    Decidable (∃ a ∈ (s : Set α), p a) := decidableExistsAndFinset

Decidability of Existential Quantification over Finite Sets as Sets

Informal description

For any finite set $s$ of type $\alpha$ and any decidable predicate $p : \alpha \to \mathrm{Prop}$, it is decidable whether there exists an element $a$ in the set corresponding to $s$ such that $p(a)$ holds.

Finset.decidableEqPiFinset instance

{β : α → Type*} [_h : ∀ a, DecidableEq (β a)] : DecidableEq (∀ a ∈ s, β a)

Full source

/-- decidable equality for functions whose domain is bounded by finsets -/
instance decidableEqPiFinset {β : α → Type*} [_h : ∀ a, DecidableEq (β a)] :
    DecidableEq (∀ a ∈ s, β a) :=
  Multiset.decidableEqPiMultiset

Decidable Equality of Functions on Finite Sets

Informal description

For any type $\alpha$, finite subset $s \subseteq \alpha$, and family of types $\beta : \alpha \to Type$ where each $\beta a$ has decidable equality, the equality of functions $f, g : \forall a \in s, \beta a$ is decidable.

List.instDecidableMapsToToSetOfDecidablePredMemSet instance

[DecidablePred (· ∈ t)] : Decidable (Set.MapsTo f s t)

Full source

instance [DecidablePred (· ∈ t)] : Decidable (Set.MapsTo f s t) :=
  inferInstanceAs (Decidable (∀ x ∈ s, f x ∈ t))

Decidability of Function Mapping on Finite Sets

Informal description

For any function $f \colon \alpha \to \beta$, finite subset $s \subseteq \alpha$, and subset $t \subseteq \beta$ where membership in $t$ is decidable, the property that $f$ maps every element of $s$ into $t$ is decidable. In other words, the statement $\forall x \in s, f(x) \in t$ can be algorithmically determined to be true or false.

List.instDecidableSurjOnToSetOfDecidableEq instance

[DecidableEq β] : Decidable (Set.SurjOn f s t')

Full source

instance [DecidableEq β] : Decidable (Set.SurjOn f s t') :=
  inferInstanceAs (Decidable (∀ x ∈ t', ∃ y ∈ s, f y = x))

Decidability of Surjectivity on Finite Sets

Informal description

For any function $f \colon \alpha \to \beta$, finite subset $s \subseteq \alpha$, and subset $t' \subseteq \beta$ where equality in $\beta$ is decidable, the property that $f$ is surjective from $s$ to $t'$ is decidable. In other words, the statement $\forall y \in t', \exists x \in s, f(x) = y$ can be algorithmically determined to be true or false.

Finset.pairwise_subtype_iff_pairwise_finset' theorem

(r : β → β → Prop) (f : α → β) : Pairwise (r on fun x : s => f x) ↔ (s : Set α).Pairwise (r on f)

Full source

theorem pairwise_subtype_iff_pairwise_finset' (r : β → β → Prop) (f : α → β) :
    PairwisePairwise (r on fun x : s => f x) ↔ (s : Set α).Pairwise (r on f) :=
  pairwise_subtype_iff_pairwise_set (s : Set α) (r on f)

Equivalence of Pairwise Relations on Finite Subsets and Their Images

Informal description

For any finite set $s$ of elements of type $\alpha$, any binary relation $r$ on a type $\beta$, and any function $f \colon \alpha \to \beta$, the following are equivalent: 1. The relation $r$ holds pairwise for all pairs of elements in the subtype corresponding to $s$ after applying $f$. 2. The relation $r$ holds pairwise for all pairs of distinct elements in the image of $s$ under $f$. In other words, for $x, y \in s$, we have $r(f(x), f(y))$ for all distinct $x, y$ if and only if $r$ holds pairwise on the set $\{f(x) \mid x \in s\}$.

Finset.pairwise_subtype_iff_pairwise_finset theorem

(r : α → α → Prop) : Pairwise (r on fun x : s => x) ↔ (s : Set α).Pairwise r

Full source

theorem pairwise_subtype_iff_pairwise_finset (r : α → α → Prop) :
    PairwisePairwise (r on fun x : s => x) ↔ (s : Set α).Pairwise r :=
  pairwise_subtype_iff_pairwise_finset' r id

Equivalence of Pairwise Relations on Finite Subsets and Their Set Images

Informal description

For any finite set $s$ of elements of type $\alpha$ and any binary relation $r$ on $\alpha$, the following are equivalent: 1. The relation $r$ holds pairwise for all pairs of elements in the subtype corresponding to $s$. 2. The relation $r$ holds pairwise for all pairs of distinct elements in the set corresponding to $s$. In other words, for $x, y \in s$, we have $r(x, y)$ for all distinct $x, y$ if and only if $r$ holds pairwise on the set $\{x \mid x \in s\}$.

Mathlib.Data.Finset.Defs

File structure

Main definitions

Tags