Lemmas on finiteness of sets

This file should contain lemmas that prove some result under the assumption of Set.Finite. If your proof has as result Set.Finite, then it should go to a more specific file.

Tags

finite sets

Properties

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

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

theorem Set.Finite.induction_to {α : Type u} {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

Induction up to a finite set S.

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

Induction up to univ.

theorem Set.sUnion_finite_eq_univ {X : Type u_1} : ⋃₀ {s : Set X | s.Finite} = univ

Infinite sets

Order properties

theorem Set.exists_min_image {α : Type u} {β : Type v} [LinearOrder β] (s : Set α) (f : α → β) (h1 : s.Finite) : s.Nonempty → ∃ a ∈ s, ∀ b ∈ s, f a ≤ f b

theorem Set.exists_max_image {α : Type u} {β : Type v} [LinearOrder β] (s : Set α) (f : α → β) (h1 : s.Finite) : s.Nonempty → ∃ a ∈ s, ∀ b ∈ s, f b ≤ f a

theorem Set.exists_lower_bound_image {α : Type u} {β : Type v} [Nonempty α] [LinearOrder β] (s : Set α) (f : α → β) (h : s.Finite) : ∃ (a : α), ∀ b ∈ s, f a ≤ f b

theorem Set.exists_upper_bound_image {α : Type u} {β : Type v} [Nonempty α] [LinearOrder β] (s : Set α) (f : α → β) (h : s.Finite) : ∃ (a : α), ∀ b ∈ s, f b ≤ f a