Documentation

Mathlib.Data.Set.Finite

Finite sets #

This file defines predicates for finite and infinite sets and provides Fintype instances for many set constructions. It also proves basic facts about finite sets and gives ways to manipulate Set.Finite expressions.

Main definitions #

Set.Finite : set α → Prop→ Prop
Set.Infinite : set α → Prop→ Prop
Set.to_finite to prove Set.Finite for a Set from a Finite instance.
Set.Finite.toFinset to noncomputably produce a Finset from a Set.Finite proof. (See Set.toFinset for a computable version.)

Implementation #

A finite set is defined to be a set whose coercion to a type has a Fintype instance. Since Set.Finite is Prop-valued, this is the mere fact that the Fintype instance exists.

There are two components to finiteness constructions. The first is Fintype instances for each construction. This gives a way to actually compute a Finset that represents the set, and these may be accessed using set.toFinset. This gets the Finset in the correct form, since otherwise Finset.univ : Finset s is a Finset for the subtype for s. The second component is "constructors" for Set.Finite that give proofs that Fintype instances exist classically given other Set.Finite proofs. Unlike the Fintype instances, these do not use any decidability instances since they do not compute anything.

Tags #

finite sets

inductive Set.Finite {α : Type u} (s : Set α) :

intro: ∀ {α : Type u} {s : Set α}, Fintype ↑s → Set.Finite s

A set is finite if there is a Finset with the same elements. This is represented as there being a Fintype instance for the set coerced to a type.

Note: this is a custom inductive type rather than Nonempty (Fintype s) so that it won't be frozen as a local instance.

Instances For

theorem Set.finite_def {α : Type u} {s : Set α} :

Set.Finite s ↔ Nonempty (Fintype ↑s)

theorem Set.Finite.nonempty_fintype {α : Type u} {s : Set α} :

Set.Finite s → Nonempty (Fintype ↑s)

Alias of the forward direction of Set.finite_def.

theorem Set.finite_coe_iff {α : Type u} {s : Set α} :

Finite ↑s ↔ Set.Finite s

theorem Set.toFinite {α : Type u} (s : Set α) [inst : Finite ↑s] :

Constructor for Set.Finite using a Finite instance.

theorem Set.Finite.ofFinset {α : Type u} {p : Set α} (s : Finset α) (H : ∀ (x : α), x ∈ s ↔ x ∈ p) :

Construct a Finite instance for a Set from a Finset with the same elements.

theorem Set.Finite.to_subtype {α : Type u} {s : Set α} (h : Set.Finite s) :

Projection of Set.Finite to its Finite instance. This is intended to be used with dot notation. See also Set.Finite.Fintype and Set.Finite.nonempty_fintype.

noncomputable def Set.Finite.fintype {α : Type u} {s : Set α} (h : Set.Finite s) :

A finite set coerced to a type is a Fintype. This is the Fintype projection for a Set.Finite.

Note that because Finite isn't a typeclass, this definition will not fire if it is made into an instance

Equations

Set.Finite.fintype h = Nonempty.some (_ : Nonempty (Fintype ↑s))

noncomputable def Set.Finite.toFinset {α : Type u} {s : Set α} (h : Set.Finite s) :

Using choice, get the Finset that represents this Set.

Equations

Set.Finite.toFinset h = Set.toFinset s

theorem Set.Finite.exists_finset {α : Type u} {s : Set α} (h : Set.Finite s) :

∃ s', ∀ (a : α), a ∈ s' ↔ a ∈ s

theorem Set.Finite.exists_finset_coe {α : Type u} {s : Set α} (h : Set.Finite s) :

∃ s', ↑s' = s

instance Set.instCanLiftSetFinsetToSetFinite {α : Type u} :

CanLift (Set α) (Finset α) Finset.toSet Set.Finite

Finite sets can be lifted to finsets.

Equations

Set.instCanLiftSetFinsetToSetFinite = { prf := (_ : ∀ (x : Set α), Set.Finite x → ∃ s', ↑s' = x) }

def Set.Infinite {α : Type u} (s : Set α) :

A set is infinite if it is not finite.

This is protected so that it does not conflict with global Infinite.

Equations

Set.Infinite s = ¬Set.Finite s

@[simp]

theorem Set.not_infinite {α : Type u} {s : Set α} :

¬Set.Infinite s ↔ Set.Finite s

theorem Set.finite_or_infinite {α : Type u} (s : Set α) :

Set.Finite s ∨ Set.Infinite s

See also finite_or_infinite, fintype_or_infinite.

Basic properties of `Set.Finite.toFinset` #

@[simp]

theorem Set.Finite.mem_toFinset {α : Type u} {s : Set α} {a : α} (h : Set.Finite s) :

a ∈ Set.Finite.toFinset h ↔ a ∈ s

@[simp]

theorem Set.Finite.coe_toFinset {α : Type u} {s : Set α} (h : Set.Finite s) :

↑(Set.Finite.toFinset h) = s

@[simp]

theorem Set.Finite.toFinset_nonempty {α : Type u} {s : Set α} (h : Set.Finite s) :

Finset.Nonempty (Set.Finite.toFinset h) ↔ Set.Nonempty s

theorem Set.Finite.coeSort_toFinset {α : Type u} {s : Set α} (h : Set.Finite s) :

{ x // x ∈ Set.Finite.toFinset h } = ↑s

Note that this is an equality of types not holding definitionally. Use wisely.

@[simp]

theorem Set.Finite.toFinset_inj {α : Type u} {s : Set α} {t : Set α} {hs : Set.Finite s} {ht : Set.Finite t} :

Set.Finite.toFinset hs = Set.Finite.toFinset ht ↔ s = t

@[simp]

theorem Set.Finite.toFinset_subset {α : Type u} {s : Set α} {hs : Set.Finite s} {t : Finset α} :

Set.Finite.toFinset hs ⊆ t ↔ s ⊆ ↑t

@[simp]

theorem Set.Finite.toFinset_ssubset {α : Type u} {s : Set α} {hs : Set.Finite s} {t : Finset α} :

Set.Finite.toFinset hs ⊂ t ↔ s ⊂ ↑t

@[simp]

theorem Set.Finite.subset_toFinset {α : Type u} {t : Set α} {ht : Set.Finite t} {s : Finset α} :

s ⊆ Set.Finite.toFinset ht ↔ ↑s ⊆ t

@[simp]

theorem Set.Finite.ssubset_toFinset {α : Type u} {t : Set α} {ht : Set.Finite t} {s : Finset α} :

s ⊂ Set.Finite.toFinset ht ↔ ↑s ⊂ t

theorem Set.Finite.toFinset_subset_toFinset {α : Type u} {s : Set α} {t : Set α} {hs : Set.Finite s} {ht : Set.Finite t} :

Set.Finite.toFinset hs ⊆ Set.Finite.toFinset ht ↔ s ⊆ t

theorem Set.Finite.toFinset_ssubset_toFinset {α : Type u} {s : Set α} {t : Set α} {hs : Set.Finite s} {ht : Set.Finite t} :

Set.Finite.toFinset hs ⊂ Set.Finite.toFinset ht ↔ s ⊂ t

theorem Set.Finite.toFinset_mono {α : Type u} {s : Set α} {t : Set α} {hs : Set.Finite s} {ht : Set.Finite t} :

s ⊆ t → Set.Finite.toFinset hs ⊆ Set.Finite.toFinset ht

Alias of the reverse direction of Set.Finite.toFinset_subset_toFinset.

theorem Set.Finite.toFinset_strictMono {α : Type u} {s : Set α} {t : Set α} {hs : Set.Finite s} {ht : Set.Finite t} :

s ⊂ t → Set.Finite.toFinset hs ⊂ Set.Finite.toFinset ht

Alias of the reverse direction of Set.Finite.toFinset_ssubset_toFinset.

@[simp]

theorem Set.Finite.toFinset_setOf {α : Type u} [inst : Fintype α] (p : α → Prop) [inst : DecidablePred p] (h : Set.Finite { x | p x }) :

Set.Finite.toFinset h = Finset.filter p Finset.univ

@[simp]

theorem Set.Finite.disjoint_toFinset {α : Type u} {s : Set α} {t : Set α} {hs : Set.Finite s} {ht : Set.Finite t} :

Disjoint (Set.Finite.toFinset hs) (Set.Finite.toFinset ht) ↔ Disjoint s t

theorem Set.Finite.toFinset_inter {α : Type u} {s : Set α} {t : Set α} [inst : DecidableEq α] (hs : Set.Finite s) (ht : Set.Finite t) (h : Set.Finite (s ∩ t)) :

Set.Finite.toFinset h = Set.Finite.toFinset hs ∩ Set.Finite.toFinset ht

theorem Set.Finite.toFinset_union {α : Type u} {s : Set α} {t : Set α} [inst : DecidableEq α] (hs : Set.Finite s) (ht : Set.Finite t) (h : Set.Finite (s ∪ t)) :

Set.Finite.toFinset h = Set.Finite.toFinset hs ∪ Set.Finite.toFinset ht

theorem Set.Finite.toFinset_diff {α : Type u} {s : Set α} {t : Set α} [inst : DecidableEq α] (hs : Set.Finite s) (ht : Set.Finite t) (h : Set.Finite (s \ t)) :

Set.Finite.toFinset h = Set.Finite.toFinset hs \ Set.Finite.toFinset ht

theorem Set.Finite.toFinset_symmDiff {α : Type u} {s : Set α} {t : Set α} [inst : DecidableEq α] (hs : Set.Finite s) (ht : Set.Finite t) (h : Set.Finite (s ∆ t)) :

Set.Finite.toFinset h = Set.Finite.toFinset hs ∆ Set.Finite.toFinset ht

theorem Set.Finite.toFinset_compl {α : Type u} {s : Set α} [inst : DecidableEq α] [inst : Fintype α] (hs : Set.Finite s) (h : Set.Finite (sᶜ)) :

Set.Finite.toFinset h = Set.Finite.toFinset hsᶜ

@[simp]

theorem Set.Finite.toFinset_empty {α : Type u} (h : Set.Finite ∅) :

Set.Finite.toFinset h = ∅

theorem Set.Finite.toFinset_univ {α : Type u} [inst : Fintype α] (h : Set.Finite Set.univ) :

Set.Finite.toFinset h = Finset.univ

@[simp]

theorem Set.Finite.toFinset_eq_empty {α : Type u} {s : Set α} {h : Set.Finite s} :

Set.Finite.toFinset h = ∅ ↔ s = ∅

@[simp]

theorem Set.Finite.toFinset_eq_univ {α : Type u} {s : Set α} [inst : Fintype α] {h : Set.Finite s} :

Set.Finite.toFinset h = Finset.univ ↔ s = Set.univ

theorem Set.Finite.toFinset_image {α : Type u} {β : Type v} {s : Set α} [inst : DecidableEq β] (f : α → β) (hs : Set.Finite s) (h : Set.Finite (f '' s)) :

Set.Finite.toFinset h = Finset.image f (Set.Finite.toFinset hs)

@[simp]

theorem Set.Finite.toFinset_range {α : Type u} {β : Type v} [inst : DecidableEq α] [inst : Fintype β] (f : β → α) (h : Set.Finite (Set.range f)) :

Set.Finite.toFinset h = Finset.image f Finset.univ

Fintype instances #

Every instance here should have a corresponding Set.Finite constructor in the next section.

instance Set.fintypeUniv {α : Type u} [inst : Fintype α] :

Fintype ↑Set.univ

Equations

Set.fintypeUniv = Fintype.ofEquiv α (Equiv.symm (Equiv.Set.univ α))

noncomputable def Set.fintypeOfFiniteUniv {α : Type u} (H : Set.Finite Set.univ) :

If (Set.univ : Set α) is finite then α is a finite type.

Equations

Set.fintypeOfFiniteUniv H = Fintype.ofEquiv (↑Set.univ) (Equiv.Set.univ α)

instance Set.fintypeUnion {α : Type u} [inst : DecidableEq α] (s : Set α) (t : Set α) [inst : Fintype ↑s] [inst : Fintype ↑t] :

Fintype ↑(s ∪ t)

Equations

Set.fintypeUnion s t = Fintype.ofFinset (Set.toFinset s ∪ Set.toFinset t) (_ : ∀ (a : α), a ∈ Set.toFinset s ∪ Set.toFinset t ↔ a ∈ s ∪ t)

instance Set.fintypeSep {α : Type u} (s : Set α) (p : α → Prop) [inst : Fintype ↑s] [inst : DecidablePred p] :

Fintype ↑{ a | a ∈ s ∧ p a }

Equations

Set.fintypeSep s p = Fintype.ofFinset (Finset.filter p (Set.toFinset s)) (_ : ∀ (a : α), a ∈ Finset.filter p (Set.toFinset s) ↔ a ∈ s ∧ p a)

instance Set.fintypeInter {α : Type u} (s : Set α) (t : Set α) [inst : DecidableEq α] [inst : Fintype ↑s] [inst : Fintype ↑t] :

Fintype ↑(s ∩ t)

Equations

Set.fintypeInter s t = Fintype.ofFinset (Set.toFinset s ∩ Set.toFinset t) (_ : ∀ (a : α), a ∈ Set.toFinset s ∩ Set.toFinset t ↔ a ∈ s ∩ t)

instance Set.fintypeInterOfLeft {α : Type u} (s : Set α) (t : Set α) [inst : Fintype ↑s] [inst : DecidablePred fun x => x ∈ t] :

Fintype ↑(s ∩ t)

A Fintype instance for set intersection where the left set has a Fintype instance.

Equations

Set.fintypeInterOfLeft s t = Fintype.ofFinset (Finset.filter (fun x => x ∈ t) (Set.toFinset s)) (_ : ∀ (a : α), a ∈ Finset.filter (fun x => x ∈ t) (Set.toFinset s) ↔ a ∈ s ∩ t)

instance Set.fintypeInterOfRight {α : Type u} (s : Set α) (t : Set α) [inst : Fintype ↑t] [inst : DecidablePred fun x => x ∈ s] :

Fintype ↑(s ∩ t)

A Fintype instance for set intersection where the right set has a Fintype instance.

Equations

Set.fintypeInterOfRight s t = Fintype.ofFinset (Finset.filter (fun x => x ∈ s) (Set.toFinset t)) (_ : ∀ (a : α), a ∈ Finset.filter (fun x => x ∈ s) (Set.toFinset t) ↔ a ∈ s ∩ t)

def Set.fintypeSubset {α : Type u} (s : Set α) {t : Set α} [inst : Fintype ↑s] [inst : DecidablePred fun x => x ∈ t] (h : t ⊆ s) :

A Fintype structure on a set defines a Fintype structure on its subset.

Equations

Set.fintypeSubset s h = Eq.mpr (_ : Fintype ↑t = Fintype ↑(s ∩ t)) (Set.fintypeInterOfLeft s t)

instance Set.fintypeDiff {α : Type u} [inst : DecidableEq α] (s : Set α) (t : Set α) [inst : Fintype ↑s] [inst : Fintype ↑t] :

Fintype ↑(s \ t)

Equations

Set.fintypeDiff s t = Fintype.ofFinset (Set.toFinset s \ Set.toFinset t) (_ : ∀ (a : α), a ∈ Set.toFinset s \ Set.toFinset t ↔ a ∈ s \ t)

instance Set.fintypeDiffLeft {α : Type u} (s : Set α) (t : Set α) [inst : Fintype ↑s] [inst : DecidablePred fun x => x ∈ t] :

Fintype ↑(s \ t)

Equations

Set.fintypeDiffLeft s t = Set.fintypeSep s fun x => x ∈ tᶜ

instance Set.fintypeUnionᵢ {α : Type u} {ι : Sort w} [inst : DecidableEq α] [inst : Fintype (PLift ι)] (f : ι → Set α) [inst : (i : ι) → Fintype ↑(f i)] :

Fintype ↑(Set.unionᵢ fun i => f i)

Equations

One or more equations did not get rendered due to their size.

instance Set.fintypeUnionₛ {α : Type u} [inst : DecidableEq α] {s : Set (Set α)} [inst : Fintype ↑s] [H : (t : ↑s) → Fintype ↑↑t] :

Fintype ↑(⋃₀ s)

Equations

Set.fintypeUnionₛ = Eq.mpr (_ : Fintype ↑(⋃₀ s) = Fintype ↑(Set.unionᵢ fun i => ↑i)) (Set.fintypeUnionᵢ fun i => ↑i)

def Set.fintypeBUnionᵢ {α : Type u} [inst : DecidableEq α] {ι : Type u_1} (s : Set ι) [inst : Fintype ↑s] (t : ι → Set α) (H : (i : ι) → i ∈ s → Fintype ↑(t i)) :

Fintype ↑(Set.unionᵢ fun x => Set.unionᵢ fun h => t x)

A union of sets with Fintype structure over a set with Fintype structure has a Fintype structure.

Equations

One or more equations did not get rendered due to their size.

instance Set.fintypeBUnionᵢ' {α : Type u} [inst : DecidableEq α] {ι : Type u_1} (s : Set ι) [inst : Fintype ↑s] (t : ι → Set α) [inst : (i : ι) → Fintype ↑(t i)] :

Fintype ↑(Set.unionᵢ fun x => Set.unionᵢ fun h => t x)

Equations

One or more equations did not get rendered due to their size.

def Set.fintypeBind {α : Type u_1} {β : Type u_1} [inst : DecidableEq β] (s : Set α) [inst : Fintype ↑s] (f : α → Set β) (H : (a : α) → a ∈ s → Fintype ↑(f a)) :

Fintype ↑(s >>= f)

If s : Set α is a set with Fintype instance and f : α → Set β→ Set β is a function such that each f a, a ∈ s∈ s, has a Fintype structure, then s >>= f has a Fintype structure.

Equations

Set.fintypeBind s f H = Set.fintypeBUnionᵢ s f H

instance Set.fintypeBind' {α : Type u_1} {β : Type u_1} [inst : DecidableEq β] (s : Set α) [inst : Fintype ↑s] (f : α → Set β) [inst : (a : α) → Fintype ↑(f a)] :

Fintype ↑(s >>= f)

Equations

Set.fintypeBind' s f = Set.fintypeBUnionᵢ' s f

instance Set.fintypeEmpty {α : Type u} :

Equations

Set.fintypeEmpty = Fintype.ofFinset ∅ (_ : ∀ (a : α), a ∈ ∅ ↔ a ∈ ∅)

instance Set.fintypeSingleton {α : Type u} (a : α) :

Fintype ↑{a}

Equations

Set.fintypeSingleton a = Fintype.ofFinset {a} (_ : ∀ (a : α), a ∈ {a} ↔ a ∈ {a})

instance Set.fintypePure {α : Type u} (a : α) :

Fintype ↑(pure a)

Equations

Set.fintypePure = Set.fintypeSingleton

instance Set.fintypeInsert {α : Type u} (a : α) (s : Set α) [inst : DecidableEq α] [inst : Fintype ↑s] :

Fintype ↑(insert a s)

A Fintype instance for inserting an element into a Set using the corresponding insert function on Finset. This requires DecidableEq α. There is also Set.fintypeInsert' when a ∈ s∈ s is decidable.

Equations

Set.fintypeInsert a s = Fintype.ofFinset (insert a (Set.toFinset s)) (_ : ∀ (a : α), a ∈ insert a (Set.toFinset s) ↔ a ∈ insert a s)

def Set.fintypeInsertOfNotMem {α : Type u} {a : α} (s : Set α) [inst : Fintype ↑s] (h : ¬a ∈ s) :

Fintype ↑(insert a s)

A Fintype structure on insert a s when inserting a new element.

Equations

One or more equations did not get rendered due to their size.

def Set.fintypeInsertOfMem {α : Type u} {a : α} (s : Set α) [inst : Fintype ↑s] (h : a ∈ s) :

Fintype ↑(insert a s)

A Fintype structure on insert a s when inserting a pre-existing element.

Equations

Set.fintypeInsertOfMem s h = Fintype.ofFinset (Set.toFinset s) (_ : ∀ (a : α), a ∈ Set.toFinset s ↔ a ∈ insert a s)

instance Set.fintypeInsert' {α : Type u} (a : α) (s : Set α) [inst : Decidable (a ∈ s)] [inst : Fintype ↑s] :

Fintype ↑(insert a s)

The Set.fintypeInsert instance requires decidable equality, but when a ∈ s∈ s is decidable for this particular a we can still get a Fintype instance by using Set.fintypeInsertOfNotMem or Set.fintypeInsertOfMem.

This instance pre-dates Set.fintypeInsert, and it is less efficient. When Set.decidableMemOfFintype is made a local instance, then this instance would override Set.fintypeInsert if not for the fact that its priority has been adjusted. See Note [lower instance priority].

Equations

Set.fintypeInsert' a s = if h : a ∈ s then Set.fintypeInsertOfMem s h else Set.fintypeInsertOfNotMem s h

instance Set.fintypeImage {α : Type u} {β : Type v} [inst : DecidableEq β] (s : Set α) (f : α → β) [inst : Fintype ↑s] :

Fintype ↑(f '' s)

Equations

Set.fintypeImage s f = Fintype.ofFinset (Finset.image f (Set.toFinset s)) (_ : ∀ (a : β), a ∈ Finset.image f (Set.toFinset s) ↔ a ∈ f '' s)

def Set.fintypeOfFintypeImage {α : Type u} {β : Type v} (s : Set α) {f : α → β} {g : β → Option α} (I : Function.IsPartialInv f g) [inst : Fintype ↑(f '' s)] :

If a function f has a partial inverse and sends a set s to a set with [Fintype] instance, then s has a Fintype structure as well.

Equations

One or more equations did not get rendered due to their size.

instance Set.fintypeRange {α : Type u} {ι : Sort w} [inst : DecidableEq α] (f : ι → α) [inst : Fintype (PLift ι)] :

Fintype ↑(Set.range f)

Equations

Set.fintypeRange f = Fintype.ofFinset (Finset.image (f ∘ PLift.down) Finset.univ) (_ : ∀ (a : α), a ∈ Finset.image (f ∘ PLift.down) Finset.univ ↔ a ∈ Set.range f)

instance Set.fintypeMap {α : Type u_1} {β : Type u_1} [inst : DecidableEq β] (s : Set α) (f : α → β) [inst : Fintype ↑s] :

Fintype ↑(f <$> s)

Equations

Set.fintypeMap = Set.fintypeImage

instance Set.fintypeLTNat (n : ℕ) :

Fintype ↑{ i | i < n }

Equations

Set.fintypeLTNat n = Fintype.ofFinset (Finset.range n) (_ : ∀ (a : ℕ), a ∈ Finset.range n ↔ a < n)

instance Set.fintypeLENat (n : ℕ) :

Fintype ↑{ i | i ≤ n }

Equations

Set.fintypeLENat n = id (Eq.mp (_ : Fintype ↑{ x | x < Nat.succ n } = Fintype ↑{ x | x ≤ n }) (Set.fintypeLTNat (n + 1)))

def Set.Nat.fintypeIio (n : ℕ) :

Fintype ↑(Set.Iio n)

This is not an instance so that it does not conflict with the one in Mathlib/Order/LocallyFinite.lean.

Equations

Set.Nat.fintypeIio n = Set.fintypeLTNat n

instance Set.fintypeProd {α : Type u} {β : Type v} (s : Set α) (t : Set β) [inst : Fintype ↑s] [inst : Fintype ↑t] :

Fintype ↑(s ×ˢ t)

Equations

Set.fintypeProd s t = Fintype.ofFinset (Set.toFinset s ×ᶠ Set.toFinset t) (_ : ∀ (a : α × β), a ∈ Set.toFinset s ×ᶠ Set.toFinset t ↔ a ∈ s ×ˢ t)

instance Set.fintypeOffDiag {α : Type u} [inst : DecidableEq α] (s : Set α) [inst : Fintype ↑s] :

Fintype ↑(Set.offDiag s)

Equations

Set.fintypeOffDiag s = Fintype.ofFinset (Finset.offDiag (Set.toFinset s)) (_ : ∀ (a : α × α), a ∈ Finset.offDiag (Set.toFinset s) ↔ a ∈ Set.offDiag s)

instance Set.fintypeImage2 {α : Type u} {β : Type v} {γ : Type x} [inst : DecidableEq γ] (f : α → β → γ) (s : Set α) (t : Set β) [hs : Fintype ↑s] [ht : Fintype ↑t] :

Fintype ↑(Set.image2 f s t)

image2 f s t is Fintype if s and t are.

Equations

Set.fintypeImage2 f s t = Eq.mpr (_ : Fintype ↑(Set.image2 f s t) = Fintype ↑((fun x => f x.fst x.snd) '' s ×ˢ t)) (Set.fintypeImage (s ×ˢ t) fun x => f x.fst x.snd)

instance Set.fintypeSeq {α : Type u} {β : Type v} [inst : DecidableEq β] (f : Set (α → β)) (s : Set α) [inst : Fintype ↑f] [inst : Fintype ↑s] :

Fintype ↑(Set.seq f s)

Equations

Set.fintypeSeq f s = Eq.mpr (_ : Fintype ↑(Set.seq f s) = Fintype ↑(Set.unionᵢ fun f => Set.unionᵢ fun h => f '' s)) (Set.fintypeBUnionᵢ' f fun x => x '' s)

instance Set.fintypeSeq' {α : Type u} {β : Type u} [inst : DecidableEq β] (f : Set (α → β)) (s : Set α) [inst : Fintype ↑f] [inst : Fintype ↑s] :

Fintype ↑(Seq.seq f fun x => s)

Equations

Set.fintypeSeq' f s = Set.fintypeSeq f s

instance Set.fintypeMemFinset {α : Type u} (s : Finset α) :

Fintype ↑{ a | a ∈ s }

Equations

Set.fintypeMemFinset s = Finset.fintypeCoeSort s

Finset #

@[simp]

theorem Finset.finite_toSet {α : Type u} (s : Finset α) :

Set.Finite ↑s

Gives a Set.Finite for the Finset coerced to a Set. This is a wrapper around Set.toFinite.

@[simp]

theorem Finset.finite_toSet_toFinset {α : Type u} (s : Finset α) :

Set.Finite.toFinset (_ : Set.Finite ↑s) = s

@[simp]

theorem Multiset.finite_toSet {α : Type u} (s : Multiset α) :

Set.Finite { x | x ∈ s }

@[simp]

theorem Multiset.finite_toSet_toFinset {α : Type u} [inst : DecidableEq α] (s : Multiset α) :

Set.Finite.toFinset (_ : Set.Finite { x | x ∈ s }) = Multiset.toFinset s

@[simp]

theorem List.finite_toSet {α : Type u} (l : List α) :

Set.Finite { x | x ∈ l }

Finite instances #

There is seemingly some overlap between the following instances and the Fintype instances in Data.Set.Finite. While every Fintype instance gives a Finite instance, those instances that depend on Fintype or Decidable instances need an additional Finite instance to be able to generally apply.

Some set instances do not appear here since they are consequences of others, for example Subtype.Finite for subsets of a finite type.

instance Finite.Set.finite_union {α : Type u} (s : Set α) (t : Set α) [inst : Finite ↑s] [inst : Finite ↑t] :

Finite ↑(s ∪ t)

Equations

@Finite.Set.finite_union = @Finite.Set.finite_union.proof_1

instance Finite.Set.finite_sep {α : Type u} (s : Set α) (p : α → Prop) [inst : Finite ↑s] :

Finite ↑{ a | a ∈ s ∧ p a }

Equations

@Finite.Set.finite_sep = @Finite.Set.finite_sep.proof_1

theorem Finite.Set.subset {α : Type u} (s : Set α) {t : Set α} [inst : Finite ↑s] (h : t ⊆ s) :

instance Finite.Set.finite_inter_of_right {α : Type u} (s : Set α) (t : Set α) [inst : Finite ↑t] :

Finite ↑(s ∩ t)

Equations

@Finite.Set.finite_inter_of_right = @Finite.Set.finite_inter_of_right.proof_1

instance Finite.Set.finite_inter_of_left {α : Type u} (s : Set α) (t : Set α) [inst : Finite ↑s] :

Finite ↑(s ∩ t)

Equations

@Finite.Set.finite_inter_of_left = @Finite.Set.finite_inter_of_left.proof_1

instance Finite.Set.finite_diff {α : Type u} (s : Set α) (t : Set α) [inst : Finite ↑s] :

Finite ↑(s \ t)

Equations

@Finite.Set.finite_diff = @Finite.Set.finite_diff.proof_1

instance Finite.Set.finite_range {α : Type u} {ι : Sort w} (f : ι → α) [inst : Finite ι] :

Finite ↑(Set.range f)

Equations

@Finite.Set.finite_range = @Finite.Set.finite_range.proof_1

instance Finite.Set.finite_unionᵢ {α : Type u} {ι : Sort w} [inst : Finite ι] (f : ι → Set α) [inst : ∀ (i : ι), Finite ↑(f i)] :

Finite ↑(Set.unionᵢ fun i => f i)

Equations

@Finite.Set.finite_unionᵢ = @Finite.Set.finite_unionᵢ.proof_1

instance Finite.Set.finite_unionₛ {α : Type u} {s : Set (Set α)} [inst : Finite ↑s] [H : ∀ (t : ↑s), Finite ↑↑t] :

Finite ↑(⋃₀ s)

Equations

@Finite.Set.finite_unionₛ = @Finite.Set.finite_unionₛ.proof_1

theorem Finite.Set.finite_bunionᵢ {α : Type u} {ι : Type u_1} (s : Set ι) [inst : Finite ↑s] (t : ι → Set α) (H : ∀ (i : ι), i ∈ s → Finite ↑(t i)) :

Finite ↑(Set.unionᵢ fun x => Set.unionᵢ fun h => t x)

instance Finite.Set.finite_bunionᵢ' {α : Type u} {ι : Type u_1} (s : Set ι) [inst : Finite ↑s] (t : ι → Set α) [inst : ∀ (i : ι), Finite ↑(t i)] :

Finite ↑(Set.unionᵢ fun x => Set.unionᵢ fun h => t x)

Equations

@Finite.Set.finite_bunionᵢ' = @Finite.Set.finite_bunionᵢ'.proof_1

instance Finite.Set.finite_bunionᵢ'' {α : Type u} {ι : Type u_1} (p : ι → Prop) [h : Finite ↑{ x | p x }] (t : ι → Set α) [inst : ∀ (i : ι), Finite ↑(t i)] :

Finite ↑(Set.unionᵢ fun x => Set.unionᵢ fun _h => t x)

Example: Finite (⋃ (i < n), f i)⋃ (i < n), f i) where f : ℕ → set α→ set α and [∀ i, Finite (f i)]∀ i, Finite (f i)] (when given instances from Data.Nat.Interval).

Equations

@Finite.Set.finite_bunionᵢ'' = @Finite.Set.finite_bunionᵢ''.proof_1

instance Finite.Set.finite_interᵢ {α : Type u} {ι : Sort u_1} [inst : Nonempty ι] (t : ι → Set α) [inst : ∀ (i : ι), Finite ↑(t i)] :

Finite ↑(Set.interᵢ fun i => t i)

Equations

@Finite.Set.finite_interᵢ = @Finite.Set.finite_interᵢ.proof_1

instance Finite.Set.finite_insert {α : Type u} (a : α) (s : Set α) [inst : Finite ↑s] :

Finite ↑(insert a s)

Equations

@Finite.Set.finite_insert = @Finite.Set.finite_insert.proof_1

instance Finite.Set.finite_image {α : Type u} {β : Type v} (s : Set α) (f : α → β) [inst : Finite ↑s] :

Finite ↑(f '' s)

Equations

@Finite.Set.finite_image = @Finite.Set.finite_image.proof_1

instance Finite.Set.finite_replacement {α : Type u} {β : Type v} [inst : Finite α] (f : α → β) :

Finite ↑{ x | ∃ x_1, f x_1 = x }

Equations

@Finite.Set.finite_replacement = @Finite.Set.finite_replacement.proof_1

instance Finite.Set.finite_prod {α : Type u} {β : Type v} (s : Set α) (t : Set β) [inst : Finite ↑s] [inst : Finite ↑t] :

Finite ↑(s ×ˢ t)

Equations

@Finite.Set.finite_prod = @Finite.Set.finite_prod.proof_1

instance Finite.Set.finite_image2 {α : Type u} {β : Type v} {γ : Type x} (f : α → β → γ) (s : Set α) (t : Set β) [inst : Finite ↑s] [inst : Finite ↑t] :

Finite ↑(Set.image2 f s t)

Equations

@Finite.Set.finite_image2 = @Finite.Set.finite_image2.proof_1

instance Finite.Set.finite_seq {α : Type u} {β : Type v} (f : Set (α → β)) (s : Set α) [inst : Finite ↑f] [inst : Finite ↑s] :

Finite ↑(Set.seq f s)

Equations

@Finite.Set.finite_seq = @Finite.Set.finite_seq.proof_1

Constructors for `set.finite` #

Every constructor here should have a corresponding Fintype instance in the previous section (or in the Fintype module).

The implementation of these constructors ideally should be no more than Set.toFinite, after possibly setting up some Fintype and classical Decidable instances.

theorem Set.Finite.of_subsingleton {α : Type u} [inst : Subsingleton α] (s : Set α) :

theorem Set.finite_univ {α : Type u} [inst : Finite α] :

Set.Finite Set.univ

theorem Set.finite_univ_iff {α : Type u} :

Set.Finite Set.univ ↔ Finite α

theorem Finite.of_finite_univ {α : Type u} :

Set.Finite Set.univ → Finite α

Alias of the forward direction of Set.finite_univ_iff.

theorem Set.Finite.union {α : Type u} {s : Set α} {t : Set α} (hs : Set.Finite s) (ht : Set.Finite t) :

Set.Finite (s ∪ t)

theorem Set.Finite.finite_of_compl {α : Type u} {s : Set α} (hs : Set.Finite s) (hsc : Set.Finite (sᶜ)) :

theorem Set.Finite.sup {α : Type u} {s : Set α} {t : Set α} :

Set.Finite s → Set.Finite t → Set.Finite (s ⊔ t)

theorem Set.Finite.sep {α : Type u} {s : Set α} (hs : Set.Finite s) (p : α → Prop) :

Set.Finite { a | a ∈ s ∧ p a }

theorem Set.Finite.inter_of_left {α : Type u} {s : Set α} (hs : Set.Finite s) (t : Set α) :

Set.Finite (s ∩ t)

theorem Set.Finite.inter_of_right {α : Type u} {s : Set α} (hs : Set.Finite s) (t : Set α) :

Set.Finite (t ∩ s)

theorem Set.Finite.inf_of_left {α : Type u} {s : Set α} (h : Set.Finite s) (t : Set α) :

Set.Finite (s ⊓ t)

theorem Set.Finite.inf_of_right {α : Type u} {s : Set α} (h : Set.Finite s) (t : Set α) :

Set.Finite (t ⊓ s)

theorem Set.Finite.subset {α : Type u} {s : Set α} (hs : Set.Finite s) {t : Set α} (ht : t ⊆ s) :

theorem Set.Finite.diff {α : Type u} {s : Set α} (hs : Set.Finite s) (t : Set α) :

Set.Finite (s \ t)

theorem Set.Finite.of_diff {α : Type u} {s : Set α} {t : Set α} (hd : Set.Finite (s \ t)) (ht : Set.Finite t) :

theorem Set.finite_unionᵢ {α : Type u} {ι : Sort w} [inst : Finite ι] {f : ι → Set α} (H : ∀ (i : ι), Set.Finite (f i)) :

Set.Finite (Set.unionᵢ fun i => f i)

theorem Set.Finite.unionₛ {α : Type u} {s : Set (Set α)} (hs : Set.Finite s) (H : ∀ (t : Set α), t ∈ s → Set.Finite t) :

Set.Finite (⋃₀ s)

theorem Set.Finite.bunionᵢ {α : Type u} {ι : Type u_1} {s : Set ι} (hs : Set.Finite s) {t : ι → Set α} (ht : ∀ (i : ι), i ∈ s → Set.Finite (t i)) :

Set.Finite (Set.unionᵢ fun i => Set.unionᵢ fun h => t i)

theorem Set.Finite.bunionᵢ' {α : Type u} {ι : Type u_1} {s : Set ι} (hs : Set.Finite s) {t : (i : ι) → i ∈ s → Set α} (ht : ∀ (i : ι) (hi : i ∈ s), Set.Finite (t i hi)) :

Set.Finite (Set.unionᵢ fun i => Set.unionᵢ fun h => t i h)

Dependent version of Finite.bunionᵢ.

theorem Set.Finite.interₛ {α : Type u_1} {s : Set (Set α)} {t : Set α} (ht : t ∈ s) (hf : Set.Finite t) :

Set.Finite (⋂₀ s)

theorem Set.Finite.bind {α : Type u_1} {β : Type u_1} {s : Set α} {f : α → Set β} (h : Set.Finite s) (hf : ∀ (a : α), a ∈ s → Set.Finite (f a)) :

Set.Finite (s >>= f)

@[simp]

theorem Set.finite_empty {α : Type u} :

@[simp]

theorem Set.finite_singleton {α : Type u} (a : α) :

theorem Set.finite_pure {α : Type u} (a : α) :

Set.Finite (pure a)

@[simp]

theorem Set.Finite.insert {α : Type u} (a : α) {s : Set α} (hs : Set.Finite s) :

Set.Finite (insert a s)

theorem Set.Finite.image {α : Type u} {β : Type v} {s : Set α} (f : α → β) (hs : Set.Finite s) :

Set.Finite (f '' s)

theorem Set.finite_range {α : Type u} {ι : Sort w} (f : ι → α) [inst : Finite ι] :

Set.Finite (Set.range f)

theorem Set.Finite.dependent_image {α : Type u} {β : Type v} {s : Set α} (hs : Set.Finite s) (F : (i : α) → i ∈ s → β) :

Set.Finite { y | ∃ x hx, y = F x hx }

theorem Set.Finite.map {α : Type u_1} {β : Type u_1} {s : Set α} (f : α → β) :

Set.Finite s → Set.Finite (f <$> s)

theorem Set.Finite.of_finite_image {α : Type u} {β : Type v} {s : Set α} {f : α → β} (h : Set.Finite (f '' s)) (hi : Set.InjOn f s) :

theorem Set.finite_of_finite_preimage {α : Type u} {β : Type v} {f : α → β} {s : Set β} (h : Set.Finite (f ⁻¹' s)) (hs : s ⊆ Set.range f) :

theorem Set.Finite.of_preimage {α : Type u} {β : Type v} {f : α → β} {s : Set β} (h : Set.Finite (f ⁻¹' s)) (hf : Function.Surjective f) :

theorem Set.Finite.preimage {α : Type u} {β : Type v} {s : Set β} {f : α → β} (I : Set.InjOn f (f ⁻¹' s)) (h : Set.Finite s) :

Set.Finite (f ⁻¹' s)

theorem Set.Finite.preimage_embedding {α : Type u} {β : Type v} {s : Set β} (f : α ↪ β) (h : Set.Finite s) :

Set.Finite (↑f ⁻¹' s)

theorem Set.finite_lt_nat (n : ℕ) :

Set.Finite { i | i < n }

theorem Set.finite_le_nat (n : ℕ) :

Set.Finite { i | i ≤ n }

theorem Set.Finite.prod {α : Type u} {β : Type v} {s : Set α} {t : Set β} (hs : Set.Finite s) (ht : Set.Finite t) :

Set.Finite (s ×ˢ t)

theorem Set.Finite.offDiag {α : Type u} {s : Set α} (hs : Set.Finite s) :

Set.Finite (Set.offDiag s)

theorem Set.Finite.image2 {α : Type u} {β : Type v} {γ : Type x} (f : α → β → γ) {s : Set α} {t : Set β} (hs : Set.Finite s) (ht : Set.Finite t) :

Set.Finite (Set.image2 f s t)

theorem Set.Finite.seq {α : Type u} {β : Type v} {f : Set (α → β)} {s : Set α} (hf : Set.Finite f) (hs : Set.Finite s) :

Set.Finite (Set.seq f s)

theorem Set.Finite.seq' {α : Type u} {β : Type u} {f : Set (α → β)} {s : Set α} (hf : Set.Finite f) (hs : Set.Finite s) :

Set.Finite (Seq.seq f fun x => s)

theorem Set.finite_mem_finset {α : Type u} (s : Finset α) :

Set.Finite { a | a ∈ s }

theorem Set.Subsingleton.finite {α : Type u} {s : Set α} (h : Set.Subsingleton s) :

theorem Set.finite_preimage_inl_and_inr {α : Type u} {β : Type v} {s : Set (α ⊕ β)} :

Set.Finite (Sum.inl ⁻¹' s) ∧ Set.Finite (Sum.inr ⁻¹' s) ↔ Set.Finite s

theorem Set.exists_finite_iff_finset {α : Type u} {p : Set α → Prop} :

(∃ s, Set.Finite s ∧ p s) ↔ ∃ s, p ↑s

theorem Set.Finite.finite_subsets {α : Type u} {a : Set α} (h : Set.Finite a) :

Set.Finite { b | b ⊆ a }

There are finitely many subsets of a given finite set

theorem Set.Finite.pi {δ : Type u_1} [inst : Finite δ] {κ : δ → Type u_2} {t : (d : δ) → Set (κ d)} (ht : ∀ (d : δ), Set.Finite (t d)) :

Set.Finite (Set.pi Set.univ t)

Finite product of finite sets is finite

theorem Set.union_finset_finite_of_range_finite {α : Type u} {β : Type v} (f : α → Finset β) (h : Set.Finite (Set.range f)) :

Set.Finite (Set.unionᵢ fun a => ↑(f a))

A finite union of finsets is finite.

theorem Set.finite_range_ite {α : Type u} {β : Type v} {p : α → Prop} [inst : DecidablePred p] {f : α → β} {g : α → β} (hf : Set.Finite (Set.range f)) (hg : Set.Finite (Set.range g)) :

Set.Finite (Set.range fun x => if p x then f x else g x)

theorem Set.finite_range_const {α : Type u} {β : Type v} {c : β} :

Set.Finite (Set.range fun x => c)

Properties #

instance Set.Finite.inhabited {α : Type u} :

Inhabited { s // Set.Finite s }

Equations

Set.Finite.inhabited = { default := { val := ∅, property := (_ : Set.Finite ∅) } }

@[simp]

theorem Set.finite_union {α : Type u} {s : Set α} {t : Set α} :

Set.Finite (s ∪ t) ↔ Set.Finite s ∧ Set.Finite t

theorem Set.finite_image_iff {α : Type u} {β : Type v} {s : Set α} {f : α → β} (hi : Set.InjOn f s) :

Set.Finite (f '' s) ↔ Set.Finite s

theorem Set.univ_finite_iff_nonempty_fintype {α : Type u} :

Set.Finite Set.univ ↔ Nonempty (Fintype α)

@[simp]

theorem Set.Finite.toFinset_singleton {α : Type u} {a : α} (ha : optParam (Set.Finite {a}) (_ : Set.Finite {a})) :

Set.Finite.toFinset ha = {a}

@[simp]

theorem Set.Finite.toFinset_insert {α : Type u} [inst : DecidableEq α] {s : Set α} {a : α} (hs : Set.Finite (insert a s)) :

Set.Finite.toFinset hs = insert a (Set.Finite.toFinset (_ : Set.Finite s))

theorem Set.Finite.toFinset_insert' {α : Type u} [inst : DecidableEq α] {a : α} {s : Set α} (hs : Set.Finite s) :

Set.Finite.toFinset (_ : Set.Finite (insert a s)) = insert a (Set.Finite.toFinset hs)

theorem Set.Finite.toFinset_prod {α : Type u} {β : Type v} {s : Set α} {t : Set β} (hs : Set.Finite s) (ht : Set.Finite t) :

Set.Finite.toFinset hs ×ᶠ Set.Finite.toFinset ht = Set.Finite.toFinset (_ : Set.Finite (s ×ˢ t))

theorem Set.Finite.toFinset_offDiag {α : Type u} {s : Set α} [inst : DecidableEq α] (hs : Set.Finite s) :

Set.Finite.toFinset (_ : Set.Finite (Set.offDiag s)) = Finset.offDiag (Set.Finite.toFinset hs)

theorem Set.Finite.fin_embedding {α : Type u} {s : Set α} (h : Set.Finite s) :

∃ n f, Set.range ↑f = s

theorem Set.Finite.fin_param {α : Type u} {s : Set α} (h : Set.Finite s) :

∃ n f, Function.Injective f ∧ Set.range f = s

theorem Set.finite_option {α : Type u} {s : Set (Option α)} :

Set.Finite s ↔ Set.Finite { x | some x ∈ s }

theorem Set.finite_image_fst_and_snd_iff {α : Type u} {β : Type v} {s : Set (α × β)} :

Set.Finite (Prod.fst '' s) ∧ Set.Finite (Prod.snd '' s) ↔ Set.Finite s

theorem Set.forall_finite_image_eval_iff {δ : Type u_1} [inst : Finite δ] {κ : δ → Type u_2} {s : Set ((d : δ) → κ d)} :

(∀ (d : δ), Set.Finite (Function.eval d '' s)) ↔ Set.Finite s

theorem Set.finite_subset_unionᵢ {α : Type u} {s : Set α} (hs : Set.Finite s) {ι : Type u_1} {t : ι → Set α} (h : s ⊆ Set.unionᵢ fun i => t i) :

∃ I, Set.Finite I ∧ s ⊆ Set.unionᵢ fun i => Set.unionᵢ fun h => t i

theorem Set.eq_finite_unionᵢ_of_finite_subset_unionᵢ {α : Type u} {ι : Type u_1} {s : ι → Set α} {t : Set α} (tfin : Set.Finite t) (h : t ⊆ Set.unionᵢ fun i => s i) :

∃ I, Set.Finite I ∧ ∃ σ, (∀ (i : ↑{ i | i ∈ I }), Set.Finite (σ i)) ∧ (∀ (i : ↑{ i | i ∈ I }), σ i ⊆ s ↑i) ∧ t = Set.unionᵢ fun i => σ i

theorem Set.Finite.induction_on {α : Type u} {C : Set α → Prop} {s : Set α} (h : Set.Finite s) (H0 : C ∅) (H1 : {a : α} → {s : Set α} → ¬a ∈ s → Set.Finite s → C s → C (insert a s)) :

C s

theorem Set.Finite.induction_on' {α : Type u} {C : Set α → Prop} {S : Set α} (h : Set.Finite S) (H0 : C ∅) (H1 : {a : α} → {s : Set α} → a ∈ S → s ⊆ S → ¬a ∈ s → C s → C (insert a s)) :

C S

Analogous to Finset.induction_on'.

theorem Set.Finite.dinduction_on {α : Type u} {C : (s : Set α) → Set.Finite s → Prop} (s : Set α) (h : Set.Finite s) (H0 : C ∅ (_ : Set.Finite ∅)) (H1 : {a : α} → {s : Set α} → ¬a ∈ s → (h : Set.Finite s) → C s h → C (insert a s) (_ : Set.Finite (insert a s))) :

C s h

theorem Set.seq_of_forall_finite_exists {γ : Type u_1} {P : γ → Set γ → Prop} (h : ∀ (t : Set γ), Set.Finite t → ∃ c, P c t) :

∃ u, (n : ℕ) → P (u n) (u '' Set.Iio n)

If P is some relation between terms of γ and sets in γ, such that every finite set t : set γ has some c : γ related to it, then there is a recursively defined sequence u in γ so u n is related to the image of {0, 1, ..., n-1} under u.

(We use this later to show sequentially compact sets are totally bounded.)

Cardinality #

theorem Set.empty_card {α : Type u} :

Fintype.card ↑∅ = 0

@[simp]

theorem Set.empty_card' {α : Type u} {h : Fintype ↑∅} :

Fintype.card ↑∅ = 0

theorem Set.card_fintypeInsertOfNotMem {α : Type u} {a : α} (s : Set α) [inst : Fintype ↑s] (h : ¬a ∈ s) :

Fintype.card ↑(insert a s) = Fintype.card ↑s + 1

@[simp]

theorem Set.card_insert {α : Type u} {a : α} (s : Set α) [inst : Fintype ↑s] (h : ¬a ∈ s) {d : Fintype ↑(insert a s)} :

Fintype.card ↑(insert a s) = Fintype.card ↑s + 1

theorem Set.card_image_of_inj_on {α : Type u} {β : Type v} {s : Set α} [inst : Fintype ↑s] {f : α → β} [inst : Fintype ↑(f '' s)] (H : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x = f y → x = y) :

Fintype.card ↑(f '' s) = Fintype.card ↑s

theorem Set.card_image_of_injective {α : Type u} {β : Type v} (s : Set α) [inst : Fintype ↑s] {f : α → β} [inst : Fintype ↑(f '' s)] (H : Function.Injective f) :

Fintype.card ↑(f '' s) = Fintype.card ↑s

@[simp]

theorem Set.card_singleton {α : Type u} (a : α) :

Fintype.card ↑{a} = 1

theorem Set.card_lt_card {α : Type u} {s : Set α} {t : Set α} [inst : Fintype ↑s] [inst : Fintype ↑t] (h : s ⊂ t) :

Fintype.card ↑s < Fintype.card ↑t

theorem Set.card_le_of_subset {α : Type u} {s : Set α} {t : Set α} [inst : Fintype ↑s] [inst : Fintype ↑t] (hsub : s ⊆ t) :

Fintype.card ↑s ≤ Fintype.card ↑t

theorem Set.eq_of_subset_of_card_le {α : Type u} {s : Set α} {t : Set α} [inst : Fintype ↑s] [inst : Fintype ↑t] (hsub : s ⊆ t) (hcard : Fintype.card ↑t ≤ Fintype.card ↑s) :

s = t

theorem Set.card_range_of_injective {α : Type u} {β : Type v} [inst : Fintype α] {f : α → β} (hf : Function.Injective f) [inst : Fintype ↑(Set.range f)] :

Fintype.card ↑(Set.range f) = Fintype.card α

theorem Set.Finite.card_toFinset {α : Type u} {s : Set α} [inst : Fintype ↑s] (h : Set.Finite s) :

Finset.card (Set.Finite.toFinset h) = Fintype.card ↑s

theorem Set.card_ne_eq {α : Type u} [inst : Fintype α] (a : α) [inst : Fintype ↑{ x | x ≠ a }] :

Fintype.card ↑{ x | x ≠ a } = Fintype.card α - 1

Infinite sets #

theorem Set.infinite_univ_iff {α : Type u} :

Set.Infinite Set.univ ↔ Infinite α

theorem Set.infinite_univ {α : Type u} [h : Infinite α] :

Set.Infinite Set.univ

theorem Set.infinite_coe_iff {α : Type u} {s : Set α} :

Infinite ↑s ↔ Set.Infinite s

theorem Set.Infinite.to_subtype {α : Type u} {s : Set α} :

Set.Infinite s → Infinite ↑s

Alias of the reverse direction of Set.infinite_coe_iff.

noncomputable def Set.Infinite.natEmbedding {α : Type u} (s : Set α) (h : Set.Infinite s) :

ℕ ↪ ↑s

Embedding of ℕ into an infinite set.

Equations

Set.Infinite.natEmbedding s h = Infinite.natEmbedding ↑s

theorem Set.Infinite.exists_subset_card_eq {α : Type u} {s : Set α} (hs : Set.Infinite s) (n : ℕ) :

∃ t, ↑t ⊆ s ∧ Finset.card t = n

theorem Set.Infinite.nonempty {α : Type u} {s : Set α} (h : Set.Infinite s) :

theorem Set.infinite_of_finite_compl {α : Type u} [inst : Infinite α] {s : Set α} (hs : Set.Finite (sᶜ)) :

theorem Set.Finite.infinite_compl {α : Type u} [inst : Infinite α] {s : Set α} (hs : Set.Finite s) :

Set.Infinite (sᶜ)

theorem Set.Infinite.mono {α : Type u} {s : Set α} {t : Set α} (h : s ⊆ t) :

Set.Infinite s → Set.Infinite t

theorem Set.Infinite.diff {α : Type u} {s : Set α} {t : Set α} (hs : Set.Infinite s) (ht : Set.Finite t) :

Set.Infinite (s \ t)

@[simp]

theorem Set.infinite_union {α : Type u} {s : Set α} {t : Set α} :

Set.Infinite (s ∪ t) ↔ Set.Infinite s ∨ Set.Infinite t

theorem Set.infinite_of_infinite_image {α : Type u} {β : Type v} (f : α → β) {s : Set α} (hs : Set.Infinite (f '' s)) :

theorem Set.infinite_image_iff {α : Type u} {β : Type v} {s : Set α} {f : α → β} (hi : Set.InjOn f s) :

Set.Infinite (f '' s) ↔ Set.Infinite s

theorem Set.infinite_of_injOn_mapsTo {α : Type u} {β : Type v} {s : Set α} {t : Set β} {f : α → β} (hi : Set.InjOn f s) (hm : Set.MapsTo f s t) (hs : Set.Infinite s) :

theorem Set.Infinite.exists_ne_map_eq_of_mapsTo {α : Type u} {β : Type v} {s : Set α} {t : Set β} {f : α → β} (hs : Set.Infinite s) (hf : Set.MapsTo f s t) (ht : Set.Finite t) :

∃ x, x ∈ s ∧ ∃ y, y ∈ s ∧ x ≠ y ∧ f x = f y

theorem Set.infinite_range_of_injective {α : Type u} {β : Type v} [inst : Infinite α] {f : α → β} (hi : Function.Injective f) :

Set.Infinite (Set.range f)

theorem Set.infinite_of_injective_forall_mem {α : Type u} {β : Type v} [inst : Infinite α] {s : Set β} {f : α → β} (hi : Function.Injective f) (hf : ∀ (x : α), f x ∈ s) :

theorem Set.Infinite.exists_nat_lt {s : Set ℕ} (hs : Set.Infinite s) (n : ℕ) :

∃ m, m ∈ s ∧ n < m

theorem Set.Infinite.exists_not_mem_finset {α : Type u} {s : Set α} (hs : Set.Infinite s) (f : Finset α) :

∃ a, a ∈ s ∧ ¬a ∈ f

theorem Set.not_injOn_infinite_finite_image {α : Type u} {β : Type v} {f : α → β} {s : Set α} (h_inf : Set.Infinite s) (h_fin : Set.Finite (f '' s)) :

¬Set.InjOn f s

Order properties #

theorem Set.finite_isTop (α : Type u_1) [inst : PartialOrder α] :

Set.Finite { x | IsTop x }

theorem Set.finite_isBot (α : Type u_1) [inst : PartialOrder α] :

Set.Finite { x | IsBot x }

theorem Set.Infinite.exists_lt_map_eq_of_mapsTo {α : Type u} {β : Type v} [inst : LinearOrder α] {s : Set α} {t : Set β} {f : α → β} (hs : Set.Infinite s) (hf : Set.MapsTo f s t) (ht : Set.Finite t) :

∃ x, x ∈ s ∧ ∃ y, y ∈ s ∧ x < y ∧ f x = f y

theorem Set.Finite.exists_lt_map_eq_of_forall_mem {α : Type u} {β : Type v} [inst : LinearOrder α] [inst : Infinite α] {t : Set β} {f : α → β} (hf : ∀ (a : α), f a ∈ t) (ht : Set.Finite t) :

∃ a b, a < b ∧ f a = f b

theorem Set.exists_min_image {α : Type u} {β : Type v} [inst : LinearOrder β] (s : Set α) (f : α → β) (h1 : Set.Finite s) :

Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (b : α), b ∈ s → f a ≤ f b

theorem Set.exists_max_image {α : Type u} {β : Type v} [inst : LinearOrder β] (s : Set α) (f : α → β) (h1 : Set.Finite s) :

Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (b : α), b ∈ s → f b ≤ f a

theorem Set.exists_lower_bound_image {α : Type u} {β : Type v} [inst : Nonempty α] [inst : LinearOrder β] (s : Set α) (f : α → β) (h : Set.Finite s) :

∃ a, ∀ (b : α), b ∈ s → f a ≤ f b

theorem Set.exists_upper_bound_image {α : Type u} {β : Type v} [inst : Nonempty α] [inst : LinearOrder β] (s : Set α) (f : α → β) (h : Set.Finite s) :

∃ a, ∀ (b : α), b ∈ s → f b ≤ f a

theorem Set.Finite.supᵢ_binfᵢ_of_monotone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [inst : Preorder ι'] [inst : Nonempty ι'] [inst : IsDirected ι' fun x x_1 => x ≤ x_1] [inst : Order.Frame α] {s : Set ι} (hs : Set.Finite s) {f : ι → ι' → α} (hf : ∀ (i : ι), i ∈ s → Monotone (f i)) :

(⨆ j, ⨅ i, ⨅ h, f i j) = ⨅ i, ⨅ h, ⨆ j, f i j

theorem Set.Finite.supᵢ_binfᵢ_of_antitone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [inst : Preorder ι'] [inst : Nonempty ι'] [inst : IsDirected ι' (Function.swap fun x x_1 => x ≤ x_1)] [inst : Order.Frame α] {s : Set ι} (hs : Set.Finite s) {f : ι → ι' → α} (hf : ∀ (i : ι), i ∈ s → Antitone (f i)) :

(⨆ j, ⨅ i, ⨅ h, f i j) = ⨅ i, ⨅ h, ⨆ j, f i j

theorem Set.Finite.infᵢ_bsupᵢ_of_monotone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [inst : Preorder ι'] [inst : Nonempty ι'] [inst : IsDirected ι' (Function.swap fun x x_1 => x ≤ x_1)] [inst : Order.Coframe α] {s : Set ι} (hs : Set.Finite s) {f : ι → ι' → α} (hf : ∀ (i : ι), i ∈ s → Monotone (f i)) :

(⨅ j, ⨆ i, ⨆ h, f i j) = ⨆ i, ⨆ h, ⨅ j, f i j

theorem Set.Finite.infᵢ_bsupᵢ_of_antitone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [inst : Preorder ι'] [inst : Nonempty ι'] [inst : IsDirected ι' fun x x_1 => x ≤ x_1] [inst : Order.Coframe α] {s : Set ι} (hs : Set.Finite s) {f : ι → ι' → α} (hf : ∀ (i : ι), i ∈ s → Antitone (f i)) :

(⨅ j, ⨆ i, ⨆ h, f i j) = ⨆ i, ⨆ h, ⨅ j, f i j

theorem Set.supᵢ_infᵢ_of_monotone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [inst : Finite ι] [inst : Preorder ι'] [inst : Nonempty ι'] [inst : IsDirected ι' fun x x_1 => x ≤ x_1] [inst : Order.Frame α] {f : ι → ι' → α} (hf : ∀ (i : ι), Monotone (f i)) :

(⨆ j, ⨅ i, f i j) = ⨅ i, ⨆ j, f i j

theorem Set.supᵢ_infᵢ_of_antitone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [inst : Finite ι] [inst : Preorder ι'] [inst : Nonempty ι'] [inst : IsDirected ι' (Function.swap fun x x_1 => x ≤ x_1)] [inst : Order.Frame α] {f : ι → ι' → α} (hf : ∀ (i : ι), Antitone (f i)) :

(⨆ j, ⨅ i, f i j) = ⨅ i, ⨆ j, f i j

theorem Set.infᵢ_supᵢ_of_monotone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [inst : Finite ι] [inst : Preorder ι'] [inst : Nonempty ι'] [inst : IsDirected ι' (Function.swap fun x x_1 => x ≤ x_1)] [inst : Order.Coframe α] {f : ι → ι' → α} (hf : ∀ (i : ι), Monotone (f i)) :

(⨅ j, ⨆ i, f i j) = ⨆ i, ⨅ j, f i j

theorem Set.infᵢ_supᵢ_of_antitone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [inst : Finite ι] [inst : Preorder ι'] [inst : Nonempty ι'] [inst : IsDirected ι' fun x x_1 => x ≤ x_1] [inst : Order.Coframe α] {f : ι → ι' → α} (hf : ∀ (i : ι), Antitone (f i)) :

(⨅ j, ⨆ i, f i j) = ⨆ i, ⨅ j, f i j

theorem Set.unionᵢ_interᵢ_of_monotone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [inst : Finite ι] [inst : Preorder ι'] [inst : IsDirected ι' fun x x_1 => x ≤ x_1] [inst : Nonempty ι'] {s : ι → ι' → Set α} (hs : ∀ (i : ι), Monotone (s i)) :

(Set.unionᵢ fun j => Set.interᵢ fun i => s i j) = Set.interᵢ fun i => Set.unionᵢ fun j => s i j

An increasing union distributes over finite intersection.

theorem Set.unionᵢ_interᵢ_of_antitone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [inst : Finite ι] [inst : Preorder ι'] [inst : IsDirected ι' (Function.swap fun x x_1 => x ≤ x_1)] [inst : Nonempty ι'] {s : ι → ι' → Set α} (hs : ∀ (i : ι), Antitone (s i)) :

(Set.unionᵢ fun j => Set.interᵢ fun i => s i j) = Set.interᵢ fun i => Set.unionᵢ fun j => s i j

A decreasing union distributes over finite intersection.

theorem Set.interᵢ_unionᵢ_of_monotone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [inst : Finite ι] [inst : Preorder ι'] [inst : IsDirected ι' (Function.swap fun x x_1 => x ≤ x_1)] [inst : Nonempty ι'] {s : ι → ι' → Set α} (hs : ∀ (i : ι), Monotone (s i)) :

(Set.interᵢ fun j => Set.unionᵢ fun i => s i j) = Set.unionᵢ fun i => Set.interᵢ fun j => s i j

An increasing intersection distributes over finite union.

theorem Set.interᵢ_unionᵢ_of_antitone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [inst : Finite ι] [inst : Preorder ι'] [inst : IsDirected ι' fun x x_1 => x ≤ x_1] [inst : Nonempty ι'] {s : ι → ι' → Set α} (hs : ∀ (i : ι), Antitone (s i)) :

(Set.interᵢ fun j => Set.unionᵢ fun i => s i j) = Set.unionᵢ fun i => Set.interᵢ fun j => s i j

A decreasing intersection distributes over finite union.

theorem Set.unionᵢ_pi_of_monotone {ι : Type u_1} {ι' : Type u_2} [inst : LinearOrder ι'] [inst : Nonempty ι'] {α : ι → Type u_3} {I : Set ι} {s : (i : ι) → ι' → Set (α i)} (hI : Set.Finite I) (hs : ∀ (i : ι), i ∈ I → Monotone (s i)) :

(Set.unionᵢ fun j => Set.pi I fun i => s i j) = Set.pi I fun i => Set.unionᵢ fun j => s i j

theorem Set.unionᵢ_univ_pi_of_monotone {ι : Type u_1} {ι' : Type u_2} [inst : LinearOrder ι'] [inst : Nonempty ι'] [inst : Finite ι] {α : ι → Type u_3} {s : (i : ι) → ι' → Set (α i)} (hs : ∀ (i : ι), Monotone (s i)) :

(Set.unionᵢ fun j => Set.pi Set.univ fun i => s i j) = Set.pi Set.univ fun i => Set.unionᵢ fun j => s i j

theorem Set.finite_range_findGreatest {α : Type u} {P : α → ℕ → Prop} [inst : (x : α) → DecidablePred (P x)] {b : ℕ} :

Set.Finite (Set.range fun x => Nat.findGreatest (P x) b)

theorem Set.Finite.exists_maximal_wrt {α : Type u} {β : Type v} [inst : PartialOrder β] (f : α → β) (s : Set α) (h : Set.Finite s) :

Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'

theorem Set.Finite.bddAbove {α : Type u} [inst : SemilatticeSup α] [inst : Nonempty α] {s : Set α} (hs : Set.Finite s) :

A finite set is bounded above.

theorem Set.Finite.bddAbove_bunionᵢ {α : Type u} {β : Type v} [inst : SemilatticeSup α] [inst : Nonempty α] {I : Set β} {S : β → Set α} (H : Set.Finite I) :

BddAbove (Set.unionᵢ fun i => Set.unionᵢ fun h => S i) ↔ ∀ (i : β), i ∈ I → BddAbove (S i)

A finite union of sets which are all bounded above is still bounded above.

theorem Set.infinite_of_not_bddAbove {α : Type u} [inst : SemilatticeSup α] [inst : Nonempty α] {s : Set α} :

¬BddAbove s → Set.Infinite s

theorem Set.Finite.bddBelow {α : Type u} [inst : SemilatticeInf α] [inst : Nonempty α] {s : Set α} (hs : Set.Finite s) :

A finite set is bounded below.

theorem Set.Finite.bddBelow_bunionᵢ {α : Type u} {β : Type v} [inst : SemilatticeInf α] [inst : Nonempty α] {I : Set β} {S : β → Set α} (H : Set.Finite I) :

BddBelow (Set.unionᵢ fun i => Set.unionᵢ fun h => S i) ↔ ∀ (i : β), i ∈ I → BddBelow (S i)

A finite union of sets which are all bounded below is still bounded below.

theorem Set.infinite_of_not_bddBelow {α : Type u} [inst : SemilatticeInf α] [inst : Nonempty α] {s : Set α} :

¬BddBelow s → Set.Infinite s

theorem Finset.bddAbove {α : Type u} [inst : SemilatticeSup α] [inst : Nonempty α] (s : Finset α) :

A finset is bounded above.

theorem Finset.bddBelow {α : Type u} [inst : SemilatticeInf α] [inst : Nonempty α] (s : Finset α) :

A finset is bounded below.

theorem Finite.of_forall_not_lt_lt {α : Type u} [inst : LinearOrder α] (h : ∀ ⦃x y z : α⦄, x < y → y < z → False) :

If a linear order does not contain any triple of elements x < y < z, then this type is finite.

theorem Set.finite_of_forall_not_lt_lt {α : Type u} [inst : LinearOrder α] {s : Set α} (h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → ∀ (z : α), z ∈ s → x < y → y < z → False) :

If a set s does not contain any triple of elements x < y < z, then s is finite.

theorem Set.finite_diff_unionᵢ_Ioo {α : Type u} [inst : LinearOrder α] (s : Set α) :

Set.Finite (s \ Set.unionᵢ fun x => Set.unionᵢ fun h => Set.unionᵢ fun y => Set.unionᵢ fun h => Set.Ioo x y)

theorem Set.finite_diff_unionᵢ_Ioo' {α : Type u} [inst : LinearOrder α] (s : Set α) :

Set.Finite (s \ Set.unionᵢ fun x => Set.Ioo ↑x.fst ↑x.snd)