Mathlib.Data.Set.Finite.Lemmas

Set.Finite.fin_embedding theorem

{s : Set α} (h : s.Finite) : ∃ (n : ℕ) (f : Fin n ↪ α), range f = s

Full source

theorem Finite.fin_embedding {s : Set α} (h : s.Finite) :
    ∃ (n : ℕ) (f : Fin n ↪ α), range f = s :=
  ⟨_, (Fintype.equivFin (h.toFinset : Set α)).symm.asEmbedding, by
    simp only [Finset.coe_sort_coe, Equiv.asEmbedding_range, Finite.coe_toFinset, setOf_mem_eq]⟩

Existence of Finite Enumeration for Finite Sets

Informal description

For any finite set $s$ in a type $\alpha$, there exists a natural number $n$ and an injective function $f : \{0, \dots, n-1\} \hookrightarrow \alpha$ such that the range of $f$ is equal to $s$.

Set.Finite.fin_param theorem

{s : Set α} (h : s.Finite) : ∃ (n : ℕ) (f : Fin n → α), Injective f ∧ range f = s

Full source

theorem Finite.fin_param {s : Set α} (h : s.Finite) :
    ∃ (n : ℕ) (f : Fin n → α), Injective f ∧ range f = s :=
  let ⟨n, f, hf⟩ := h.fin_embedding
  ⟨n, f, f.injective, hf⟩

Existence of Finite Parameterization for Finite Sets

Informal description

For any finite set $s$ in a type $\alpha$, there exists a natural number $n$ and an injective function $f \colon \{0, \dots, n-1\} \to \alpha$ such that the range of $f$ is equal to $s$.

Set.Finite.induction_to theorem

 {C : Set α → Prop} {S : Set α} (h : S.Finite) (S0 : Set α) (hS0 : S0 ⊆ S) (H0 : C S0)
  (H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)) : C S

Full source

/-- Induction up to a finite set `S`. -/
theorem Finite.induction_to {C : Set α → Prop} {S : Set α} (h : S.Finite)
    (S0 : Set α) (hS0 : S0 ⊆ S) (H0 : C S0) (H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)) :
    C S := by
  have : Finite S := Finite.to_subtype h
  have : Finite {T : Set α // T ⊆ S} := Finite.of_equiv (Set S) (Equiv.Set.powerset S).symm
  rw [← Subtype.coe_mk (p := (· ⊆ S)) _ le_rfl]
  rw [← Subtype.coe_mk (p := (· ⊆ S)) _ hS0] at H0
  refine Finite.to_wellFoundedGT.wf.induction_bot' (fun s hs hs' ↦ ?_) H0
  obtain ⟨a, ⟨ha1, ha2⟩, ha'⟩ := H1 s (ssubset_of_ne_of_subset hs s.2) hs'
  exact ⟨⟨insert a s.1, insert_subset ha1 s.2⟩, Set.ssubset_insert ha2, ha'⟩

Finite Set Induction Principle

Informal description

Let $S$ be a finite subset of a type $\alpha$, and let $C$ be a predicate on subsets of $\alpha$. Suppose: 1. $S_0$ is a subset of $S$ and $C(S_0)$ holds. 2. For any proper subset $s \subset S$ satisfying $C(s)$, there exists an element $a \in S \setminus s$ such that $C(s \cup \{a\})$ holds. Then $C(S)$ holds.

Set.Finite.induction_to_univ theorem

 [Finite α] {C : Set α → Prop} (S0 : Set α) (H0 : C S0) (H1 : ∀ S ≠ univ, C S → ∃ a ∉ S, C (insert a S)) : C univ

Full source

/-- Induction up to `univ`. -/
theorem Finite.induction_to_univ [Finite α] {C : Set α → Prop} (S0 : Set α)
    (H0 : C S0) (H1 : ∀ S ≠ univ, C S → ∃ a ∉ S, C (insert a S)) : C univ :=
  finite_univ.induction_to S0 (subset_univ S0) H0 (by simpa [ssubset_univ_iff])

Finite Universal Set Induction Principle

Informal description

Let $\alpha$ be a finite type and $C$ be a predicate on subsets of $\alpha$. Suppose: 1. $C(S_0)$ holds for some subset $S_0$ of $\alpha$. 2. For any proper subset $S \subset \text{univ}$ (where $\text{univ} = \{x \mid x \in \alpha\}$) satisfying $C(S)$, there exists an element $a \in \text{univ} \setminus S$ such that $C(S \cup \{a\})$ holds. Then $C(\text{univ})$ holds.

Set.exists_min_image theorem

[LinearOrder β] (s : Set α) (f : α → β) (h1 : s.Finite) : s.Nonempty → ∃ a ∈ s, ∀ b ∈ s, f a ≤ f b

Full source

theorem exists_min_image [LinearOrder β] (s : Set α) (f : α → β) (h1 : s.Finite) :
    s.Nonempty → ∃ a ∈ s, ∀ b ∈ s, f a ≤ f b
  | ⟨x, hx⟩ => by
    simpa only [exists_prop, Finite.mem_toFinset] using
      h1.toFinset.exists_min_image f ⟨x, h1.mem_toFinset.2 hx⟩

Existence of Minimum Image in Finite Sets

Informal description

Let $s$ be a nonempty finite subset of a type $\alpha$, and let $f : \alpha \to \beta$ be a function where $\beta$ is a linearly ordered type. Then there exists an element $a \in s$ such that for all $b \in s$, $f(a) \leq f(b)$.

Set.exists_max_image theorem

[LinearOrder β] (s : Set α) (f : α → β) (h1 : s.Finite) : s.Nonempty → ∃ a ∈ s, ∀ b ∈ s, f b ≤ f a

Full source

theorem exists_max_image [LinearOrder β] (s : Set α) (f : α → β) (h1 : s.Finite) :
    s.Nonempty → ∃ a ∈ s, ∀ b ∈ s, f b ≤ f a
  | ⟨x, hx⟩ => by
    simpa only [exists_prop, Finite.mem_toFinset] using
      h1.toFinset.exists_max_image f ⟨x, h1.mem_toFinset.2 hx⟩

Existence of Maximum Image in Finite Sets

Informal description

Let $s$ be a nonempty finite subset of a type $\alpha$, and let $f : \alpha \to \beta$ be a function where $\beta$ is a linearly ordered type. Then there exists an element $a \in s$ such that for all $b \in s$, $f(b) \leq f(a)$.

Set.exists_lower_bound_image theorem

[Nonempty α] [LinearOrder β] (s : Set α) (f : α → β) (h : s.Finite) : ∃ a : α, ∀ b ∈ s, f a ≤ f b

Full source

theorem exists_lower_bound_image [Nonempty α] [LinearOrder β] (s : Set α) (f : α → β)
    (h : s.Finite) : ∃ a : α, ∀ b ∈ s, f a ≤ f b := by
  rcases s.eq_empty_or_nonempty with rfl | hs
  · exact ‹Nonempty α›.elim fun a => ⟨a, fun _ => False.elim⟩
  · rcases Set.exists_min_image s f h hs with ⟨x₀, _, hx₀⟩
    exact ⟨x₀, fun x hx => hx₀ x hx⟩

Existence of Lower Bound for Images of Finite Sets

Informal description

Let $\alpha$ be a nonempty type and $\beta$ be a linearly ordered type. For any finite subset $s \subseteq \alpha$ and any function $f : \alpha \to \beta$, there exists an element $a \in \alpha$ such that for all $b \in s$, $f(a) \leq f(b)$.

Set.exists_upper_bound_image theorem

[Nonempty α] [LinearOrder β] (s : Set α) (f : α → β) (h : s.Finite) : ∃ a : α, ∀ b ∈ s, f b ≤ f a

Full source

theorem exists_upper_bound_image [Nonempty α] [LinearOrder β] (s : Set α) (f : α → β)
    (h : s.Finite) : ∃ a : α, ∀ b ∈ s, f b ≤ f a :=
  exists_lower_bound_image (β := βᵒᵈ) s f h

Existence of Upper Bound for Images of Finite Sets

Informal description

Let $\alpha$ be a nonempty type and $\beta$ be a linearly ordered type. For any finite subset $s \subseteq \alpha$ and any function $f : \alpha \to \beta$, there exists an element $a \in \alpha$ such that for all $b \in s$, $f(b) \leq f(a)$.

Tags