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 ↪ α), Set.range ⇑f = s

theorem Set.Finite.fin_param {α : Type u} {s : Set α} (h : s.Finite) : ∃ (n : ℕ) (f : Fin n → α), Function.Injective f ∧ Set.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 ≠ Set.univ → C S → ∃ a ∉ S, C (insert a S)) : C Set.univ

Induction up to 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