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 α → PropSet.Infinite : Set α → PropSet.toFiniteto proveSet.Finitefor aSetfrom aFiniteinstance.Set.Finite.toFinsetto noncomputably produce aFinsetfrom aSet.Finiteproof. (SeeSet.toFinsetfor 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
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.
- intro: ∀ {α : Type u} {s : Set α}, Fintype ↑s → Set.Finite s
Instances For
Alias of the forward direction of Set.finite_def.
Constructor for Set.Finite using a Finite instance.
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.
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))
Instances For
@[simp]
theorem
Set.toFinite_toFinset
{α : Type u}
(s : Set α)
[Fintype ↑s]
:
Set.Finite.toFinset (_ : Set.Finite s) = Set.toFinset s
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
Instances For
@[simp]
Alias of the reverse direction of Set.not_infinite.
See also finite_or_infinite, fintypeOrInfinite.
Basic properties of Set.Finite.toFinset #
@[simp]
theorem
Set.Finite.mem_toFinset
{α : Type u}
{s : Set α}
{a : α}
(hs : Set.Finite s)
:
a ∈ Set.Finite.toFinset hs ↔ a ∈ s
@[simp]
theorem
Set.Finite.coe_toFinset
{α : Type u}
{s : Set α}
(hs : Set.Finite s)
:
↑(Set.Finite.toFinset hs) = s
@[simp]
theorem
Set.Finite.toFinset_nonempty
{α : Type u}
{s : Set α}
(hs : Set.Finite s)
:
(Set.Finite.toFinset hs).Nonempty ↔ Set.Nonempty s
theorem
Set.Finite.coeSort_toFinset
{α : Type u}
{s : Set α}
(hs : Set.Finite s)
:
{ x : α // x ∈ Set.Finite.toFinset hs } = ↑s
Note that this is an equality of types not holding definitionally. Use wisely.
@[simp]
theorem
Set.Finite.subtypeEquivToFinset_symm_apply_coe
{α : Type u}
{s : Set α}
(hs : Set.Finite s)
(b : { b : α // (fun (x : α) => x ∈ Set.Finite.toFinset hs) b })
:
↑((Set.Finite.subtypeEquivToFinset hs).symm b) = ↑b
@[simp]
theorem
Set.Finite.subtypeEquivToFinset_apply_coe
{α : Type u}
{s : Set α}
(hs : Set.Finite s)
(a : { a : α // (fun (x : α) => x ∈ s) a })
:
↑((Set.Finite.subtypeEquivToFinset hs) a) = ↑a
def
Set.Finite.subtypeEquivToFinset
{α : Type u}
{s : Set α}
(hs : Set.Finite s)
:
{ x : α // x ∈ s } ≃ { x : α // x ∈ Set.Finite.toFinset hs }
The identity map, bundled as an equivalence between the subtypes of s : Set α and of
h.toFinset : Finset α, where h is a proof of finiteness of s.
Equations
- Set.Finite.subtypeEquivToFinset hs = Equiv.subtypeEquiv (Equiv.refl α) (_ : ∀ (x : α), x ∈ s ↔ x ∈ Set.Finite.toFinset hs)
Instances For
@[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}
[Fintype α]
(p : α → Prop)
[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 α}
[DecidableEq α]
(hs : Set.Finite s)
(ht : Set.Finite t)
(h : Set.Finite (s ∩ t))
:
theorem
Set.Finite.toFinset_union
{α : Type u}
{s : Set α}
{t : Set α}
[DecidableEq α]
(hs : Set.Finite s)
(ht : Set.Finite t)
(h : Set.Finite (s ∪ t))
:
theorem
Set.Finite.toFinset_diff
{α : Type u}
{s : Set α}
{t : Set α}
[DecidableEq α]
(hs : Set.Finite s)
(ht : Set.Finite t)
(h : Set.Finite (s \ t))
:
theorem
Set.Finite.toFinset_symmDiff
{α : Type u}
{s : Set α}
{t : Set α}
[DecidableEq α]
(hs : Set.Finite s)
(ht : Set.Finite t)
(h : Set.Finite (symmDiff s t))
:
theorem
Set.Finite.toFinset_compl
{α : Type u}
{s : Set α}
[DecidableEq α]
[Fintype α]
(hs : Set.Finite s)
(h : Set.Finite sᶜ)
:
theorem
Set.Finite.toFinset_univ
{α : Type u}
[Fintype α]
(h : Set.Finite Set.univ)
:
Set.Finite.toFinset h = Finset.univ
@[simp]
@[simp]
theorem
Set.Finite.toFinset_eq_univ
{α : Type u}
{s : Set α}
[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 α}
[DecidableEq β]
(f : α → β)
(hs : Set.Finite s)
(h : Set.Finite (f '' s))
:
theorem
Set.Finite.toFinset_range
{α : Type u}
{β : Type v}
[DecidableEq α]
[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.
Equations
- Set.fintypeUniv = Fintype.ofEquiv α (Equiv.Set.univ α).symm
If (Set.univ : Set α) is finite then α is a finite type.
Equations
- Set.fintypeOfFiniteUniv H = Fintype.ofEquiv (↑Set.univ) (Equiv.Set.univ α)
Instances For
instance
Set.fintypeUnion
{α : Type u}
[DecidableEq α]
(s : Set α)
(t : Set α)
[Fintype ↑s]
[Fintype ↑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)
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 α)
[DecidableEq α]
[Fintype ↑s]
[Fintype ↑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)
def
Set.fintypeSubset
{α : Type u}
(s : Set α)
{t : Set α}
[Fintype ↑s]
[DecidablePred fun (x : α) => x ∈ t]
(h : t ⊆ s)
:
Fintype ↑t
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)
Instances For
instance
Set.fintypeDiff
{α : Type u}
[DecidableEq α]
(s : Set α)
(t : Set α)
[Fintype ↑s]
[Fintype ↑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 α)
[Fintype ↑s]
[DecidablePred fun (x : α) => x ∈ t]
:
Equations
- Set.fintypeDiffLeft s t = Set.fintypeSep s fun (x : α) => x ∈ tᶜ
instance
Set.fintypeiUnion
{α : Type u}
{ι : Sort w}
[DecidableEq α]
[Fintype (PLift ι)]
(f : ι → Set α)
[(i : ι) → Fintype ↑(f i)]
:
Fintype ↑(⋃ (i : ι), f i)
Equations
- One or more equations did not get rendered due to their size.
def
Set.fintypeBiUnion
{α : Type u}
[DecidableEq α]
{ι : Type u_1}
(s : Set ι)
[Fintype ↑s]
(t : ι → Set α)
(H : (i : ι) → i ∈ s → Fintype ↑(t i))
:
Fintype ↑(⋃ x ∈ s, 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.
Instances For
instance
Set.fintypeBiUnion'
{α : Type u}
[DecidableEq α]
{ι : Type u_1}
(s : Set ι)
[Fintype ↑s]
(t : ι → Set α)
[(i : ι) → Fintype ↑(t i)]
:
Fintype ↑(⋃ x ∈ s, t x)
Equations
- One or more equations did not get rendered due to their size.
def
Set.fintypeBind
{α : Type u_1}
{β : Type u_1}
[DecidableEq β]
(s : Set α)
[Fintype ↑s]
(f : α → Set β)
(H : (a : α) → a ∈ s → Fintype ↑(f a))
:
If s : Set α is a set with Fintype instance and f : α → Set β is a function such that
each f a, a ∈ s, has a Fintype structure, then s >>= f has a Fintype structure.
Equations
- Set.fintypeBind s f H = Set.fintypeBiUnion s f H
Instances For
instance
Set.fintypeBind'
{α : Type u_1}
{β : Type u_1}
[DecidableEq β]
(s : Set α)
[Fintype ↑s]
(f : α → Set β)
[(a : α) → Fintype ↑(f a)]
:
Equations
- Set.fintypeBind' s f = Set.fintypeBiUnion' s f
Equations
- Set.fintypeSingleton a = Fintype.ofFinset {a} (_ : ∀ (a_1 : α), a_1 ∈ {a} ↔ a_1 ∈ {a})
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 is decidable.
Equations
- Set.fintypeInsert a s = Fintype.ofFinset (insert a (Set.toFinset s)) (_ : ∀ (a_1 : α), a_1 ∈ insert a (Set.toFinset s) ↔ a_1 ∈ 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_1 : α), a_1 ∈ Set.toFinset s ↔ a_1 ∈ insert a s)
Instances For
The Set.fintypeInsert instance requires decidable equality, but when a ∈ 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}
[DecidableEq β]
(s : Set α)
(f : α → β)
[Fintype ↑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)
[Fintype ↑(f '' s)]
:
Fintype ↑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.
Instances For
instance
Set.fintypeRange
{α : Type u}
{ι : Sort w}
[DecidableEq α]
(f : ι → α)
[Fintype (PLift ι)]
:
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}
[DecidableEq β]
(s : Set α)
(f : α → β)
[Fintype ↑s]
:
Equations
- Set.fintypeMap = Set.fintypeImage
Equations
- Set.fintypeLTNat n = Fintype.ofFinset (Finset.range n) (_ : ∀ (a : ℕ), a ∈ Finset.range n ↔ a < n)
This is not an instance so that it does not conflict with the one
in Mathlib/Order/LocallyFinite.lean.
Equations
Instances For
instance
Set.fintypeProd
{α : Type u}
{β : Type v}
(s : Set α)
(t : Set β)
[Fintype ↑s]
[Fintype ↑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}
[DecidableEq α]
(s : Set α)
[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}
[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.1 x.2) '' s ×ˢ t)) (Set.fintypeImage (s ×ˢ t) fun (x : α × β) => f x.1 x.2)
instance
Set.fintypeSeq'
{α : Type u}
{β : Type u}
[DecidableEq β]
(f : Set (α → β))
(s : Set α)
[Fintype ↑f]
[Fintype ↑s]
:
Equations
- Set.fintypeSeq' f s = Set.fintypeSeq f s
Equations
theorem
Equiv.set_finite_iff
{α : Type u}
{β : Type v}
{s : Set α}
{t : Set β}
(hst : ↑s ≃ ↑t)
:
Set.Finite s ↔ Set.Finite t
Finset #
@[simp]
Gives a Set.Finite for the Finset coerced to a Set.
This is a wrapper around Set.toFinite.
theorem
Finset.finite_toSet_toFinset
{α : Type u}
(s : Finset α)
:
Set.Finite.toFinset (_ : Set.Finite ↑s) = s
@[simp]
@[simp]
theorem
Multiset.finite_toSet_toFinset
{α : Type u}
[DecidableEq α]
(s : Multiset α)
:
Set.Finite.toFinset (_ : Set.Finite {x : α | x ∈ s}) = Multiset.toFinset s
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_biUnion''
{α : Type u}
{ι : Type u_1}
(p : ι → Prop)
[h : Finite ↑{x : ι | p x}]
(t : ι → Set α)
[∀ (i : ι), Finite ↑(t i)]
:
Finite ↑(⋃ (x : ι), ⋃ (_ : p x), t x)
Example: Finite (⋃ (i < n), f i) where f : ℕ → Set α and [∀ i, Finite (f i)]
(when given instances from Data.Nat.Interval).
instance
Finite.Set.finite_image2
{α : Type u}
{β : Type v}
{γ : Type x}
(f : α → β → γ)
(s : Set α)
(t : Set β)
[Finite ↑s]
[Finite ↑t]
:
Finite ↑(Set.image2 f s t)
Equations
- (_ : Finite ↑(Set.image2 f s t)) = (_ : Finite ↑(Set.image2 f s t))
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.
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ᶜ)
:
Finite α
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.Infinite.mono
{α : Type u}
{s : Set α}
{t : Set α}
(h : s ⊆ t)
:
Set.Infinite s → Set.Infinite t
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_iUnion
{α : Type u}
{ι : Sort w}
[Finite ι]
{f : ι → Set α}
(H : ∀ (i : ι), Set.Finite (f i))
:
Set.Finite (⋃ (i : ι), f i)
theorem
Set.Finite.sUnion
{α : Type u}
{s : Set (Set α)}
(hs : Set.Finite s)
(H : ∀ t ∈ s, Set.Finite t)
:
Set.Finite (⋃₀ s)
theorem
Set.Finite.biUnion
{α : Type u}
{ι : Type u_1}
{s : Set ι}
(hs : Set.Finite s)
{t : ι → Set α}
(ht : ∀ i ∈ s, Set.Finite (t i))
:
Set.Finite (⋃ i ∈ s, t i)
theorem
Set.Finite.biUnion'
{α : 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 (⋃ (i : ι), ⋃ (h : i ∈ s), t i h)
Dependent version of Finite.biUnion.
theorem
Set.Finite.sInter
{α : Type u_1}
{s : Set (Set α)}
{t : Set α}
(ht : t ∈ s)
(hf : Set.Finite t)
:
Set.Finite (⋂₀ s)
theorem
Set.Finite.iUnion
{α : Type u}
{ι : Type u_1}
{s : ι → Set α}
{t : Set ι}
(ht : Set.Finite t)
(hs : ∀ i ∈ t, Set.Finite (s i))
(he : ∀ i ∉ t, s i = ∅)
:
Set.Finite (⋃ (i : ι), s i)
If sets s i are finite for all i from a finite set t and are empty for i ∉ t, then the
union ⋃ i, s i is a finite set.
theorem
Set.Finite.bind
{α : Type u_1}
{β : Type u_1}
{s : Set α}
{f : α → Set β}
(h : Set.Finite s)
(hf : ∀ a ∈ s, Set.Finite (f a))
:
Set.Finite (s >>= f)
@[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.of_surjOn
{α : Type u}
{β : Type v}
{s : Set α}
{t : Set β}
(f : α → β)
(hf : Set.SurjOn f s t)
(hs : Set.Finite s)
:
theorem
Set.Finite.dependent_image
{α : Type u}
{β : Type v}
{s : Set α}
(hs : Set.Finite s)
(F : (i : α) → i ∈ s → β)
:
Set.Finite {y : β | ∃ (x : α) (hx : x ∈ s), F x hx = y}
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}
{f : α → β}
{s : Set β}
(I : Set.InjOn f (f ⁻¹' s))
(h : Set.Finite s)
:
Set.Finite (f ⁻¹' s)
theorem
Set.Infinite.preimage
{α : Type u}
{β : Type v}
{f : α → β}
{s : Set β}
(hs : Set.Infinite s)
(hf : s ⊆ Set.range f)
:
Set.Infinite (f ⁻¹' s)
theorem
Set.Infinite.preimage'
{α : Type u}
{β : Type v}
{f : α → β}
{s : Set β}
(hs : Set.Infinite (s ∩ Set.range f))
:
Set.Infinite (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.surjOn_iff_bijOn_of_mapsTo
{α : Type u}
{s : Set α}
{f : α → α}
(hs : Set.Finite s)
(hm : Set.MapsTo f s s)
:
Set.SurjOn f s s ↔ Set.BijOn f s s
theorem
Set.Finite.injOn_iff_bijOn_of_mapsTo
{α : Type u}
{s : Set α}
{f : α → α}
(hs : Set.Finite s)
(hm : Set.MapsTo f s s)
:
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.of_prod_left
{α : Type u}
{β : Type v}
{s : Set α}
{t : Set β}
(h : Set.Finite (s ×ˢ t))
:
Set.Nonempty t → Set.Finite s
theorem
Set.Finite.of_prod_right
{α : Type u}
{β : Type v}
{s : Set α}
{t : Set β}
(h : Set.Finite (s ×ˢ t))
:
Set.Nonempty s → Set.Finite t
theorem
Set.Infinite.prod_left
{α : Type u}
{β : Type v}
{s : Set α}
{t : Set β}
(hs : Set.Infinite s)
(ht : Set.Nonempty t)
:
Set.Infinite (s ×ˢ t)
theorem
Set.Infinite.prod_right
{α : Type u}
{β : Type v}
{s : Set α}
{t : Set β}
(ht : Set.Infinite t)
(hs : Set.Nonempty s)
:
Set.Infinite (s ×ˢ t)
theorem
Set.infinite_prod
{α : Type u}
{β : Type v}
{s : Set α}
{t : Set β}
:
Set.Infinite (s ×ˢ t) ↔ Set.Infinite s ∧ Set.Nonempty t ∨ Set.Infinite t ∧ Set.Nonempty s
theorem
Set.finite_prod
{α : Type u}
{β : Type v}
{s : Set α}
{t : Set β}
:
Set.Finite (s ×ˢ t) ↔ (Set.Finite s ∨ t = ∅) ∧ (Set.Finite t ∨ s = ∅)
theorem
Set.Finite.image2
{α : Type u}
{β : Type v}
{γ : Type x}
{s : Set α}
{t : Set β}
(f : α → β → γ)
(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 : Unit) => 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 α), Set.Finite s ∧ p s) ↔ ∃ (s : Finset α), p ↑s
theorem
Set.Finite.finite_subsets
{α : Type u}
{a : Set α}
(h : Set.Finite a)
:
Set.Finite {b : Set α | b ⊆ a}
There are finitely many subsets of a given finite set
theorem
Set.Finite.pi
{ι : Type u_1}
[Finite ι]
{κ : ι → Type u_2}
{t : (i : ι) → Set (κ i)}
(ht : ∀ (i : ι), Set.Finite (t i))
:
Set.Finite (Set.pi Set.univ t)
Finite product of finite sets is finite
theorem
Set.Finite.pi'
{ι : Type u_1}
[Finite ι]
{κ : ι → Type u_2}
{t : (i : ι) → Set (κ i)}
(ht : ∀ (i : ι), Set.Finite (t i))
:
Set.Finite {f : (i : ι) → κ i | ∀ (i : ι), f i ∈ t i}
Finite product of finite sets is finite. Note this is a variant of Set.Finite.pi without the
extra i ∈ univ binder.
theorem
Set.union_finset_finite_of_range_finite
{α : Type u}
{β : Type v}
(f : α → Finset β)
(h : Set.Finite (Set.range f))
:
Set.Finite (⋃ (a : α), ↑(f a))
A finite union of finsets is finite.
theorem
Set.finite_range_ite
{α : Type u}
{β : Type v}
{p : α → Prop}
[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 #
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 α)
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}
[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}
[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 α}
[DecidableEq α]
(hs : Set.Finite s)
:
Set.Finite.toFinset (_ : Set.Finite (Set.offDiag s)) = Finset.offDiag (Set.Finite.toFinset hs)
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}
[Finite δ]
{κ : δ → Type u_2}
{s : Set ((d : δ) → κ d)}
:
(∀ (d : δ), Set.Finite (Function.eval d '' s)) ↔ Set.Finite s
theorem
Set.finite_subset_iUnion
{α : Type u}
{s : Set α}
(hs : Set.Finite s)
{ι : Type u_1}
{t : ι → Set α}
(h : s ⊆ ⋃ (i : ι), t i)
:
∃ (I : Set ι), Set.Finite I ∧ s ⊆ ⋃ i ∈ I, t i
theorem
Set.eq_finite_iUnion_of_finite_subset_iUnion
{α : Type u}
{ι : Type u_1}
{s : ι → Set α}
{t : Set α}
(tfin : Set.Finite t)
(h : t ⊆ ⋃ (i : ι), s 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)
:
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.card_fintypeInsertOfNotMem
{α : Type u}
{a : α}
(s : Set α)
[Fintype ↑s]
(h : a ∉ s)
:
Fintype.card ↑(insert a s) = Fintype.card ↑s + 1
@[simp]
theorem
Set.card_insert
{α : Type u}
{a : α}
(s : Set α)
[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 α}
[Fintype ↑s]
{f : α → β}
[Fintype ↑(f '' s)]
(H : ∀ x ∈ s, ∀ 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 α)
[Fintype ↑s]
{f : α → β}
[Fintype ↑(f '' s)]
(H : Function.Injective f)
:
Fintype.card ↑(f '' s) = Fintype.card ↑s
theorem
Set.card_lt_card
{α : Type u}
{s : Set α}
{t : Set α}
[Fintype ↑s]
[Fintype ↑t]
(h : s ⊂ t)
:
Fintype.card ↑s < Fintype.card ↑t
theorem
Set.card_le_card
{α : Type u}
{s : Set α}
{t : Set α}
[Fintype ↑s]
[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 α}
[Fintype ↑s]
[Fintype ↑t]
(hsub : s ⊆ t)
(hcard : Fintype.card ↑t ≤ Fintype.card ↑s)
:
s = t
theorem
Set.card_range_of_injective
{α : Type u}
{β : Type v}
[Fintype α]
{f : α → β}
(hf : Function.Injective f)
[Fintype ↑(Set.range f)]
:
Fintype.card ↑(Set.range f) = Fintype.card α
theorem
Set.Finite.card_toFinset
{α : Type u}
{s : Set α}
[Fintype ↑s]
(h : Set.Finite s)
:
(Set.Finite.toFinset h).card = Fintype.card ↑s
theorem
Set.card_ne_eq
{α : Type u}
[Fintype α]
(a : α)
[Fintype ↑{x : α | x ≠ a}]
:
Fintype.card ↑{x : α | x ≠ a} = Fintype.card α - 1
Infinite sets #
Alias of the reverse direction of Set.infinite_coe_iff.
theorem
Set.Infinite.exists_not_mem_finite
{α : Type u}
{s : Set α}
{t : Set α}
(hs : Set.Infinite s)
(ht : Set.Finite t)
:
∃ a ∈ s, a ∉ t
theorem
Set.Infinite.exists_not_mem_finset
{α : Type u}
{s : Set α}
(hs : Set.Infinite s)
(t : Finset α)
:
∃ a ∈ s, a ∉ t
theorem
Set.Finite.exists_not_mem
{α : Type u}
{s : Set α}
[Infinite α]
(hs : Set.Finite s)
:
∃ (a : α), a ∉ s
Embedding of ℕ into an infinite set.
Equations
Instances For
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_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.image
{α : Type u}
{β : Type v}
{s : Set α}
{f : α → β}
(hi : Set.InjOn f s)
:
Set.Infinite s → Set.Infinite (f '' s)
Alias of the reverse direction of Set.infinite_image_iff.
theorem
Set.Infinite.image2_left
{α : Type u}
{β : Type v}
{γ : Type x}
{f : α → β → γ}
{s : Set α}
{t : Set β}
{b : β}
(hs : Set.Infinite s)
(hb : b ∈ t)
(hf : Set.InjOn (fun (a : α) => f a b) s)
:
Set.Infinite (Set.image2 f s t)
theorem
Set.Infinite.image2_right
{α : Type u}
{β : Type v}
{γ : Type x}
{f : α → β → γ}
{s : Set α}
{t : Set β}
{a : α}
(ht : Set.Infinite t)
(ha : a ∈ s)
(hf : Set.InjOn (f a) t)
:
Set.Infinite (Set.image2 f s t)
theorem
Set.infinite_image2
{α : Type u}
{β : Type v}
{γ : Type x}
{f : α → β → γ}
{s : Set α}
{t : Set β}
(hfs : ∀ b ∈ t, Set.InjOn (fun (a : α) => f a b) s)
(hft : ∀ a ∈ s, Set.InjOn (f a) t)
:
Set.Infinite (Set.image2 f s t) ↔ Set.Infinite s ∧ Set.Nonempty t ∨ Set.Infinite t ∧ Set.Nonempty s
theorem
Set.finite_image2
{α : Type u}
{β : Type v}
{γ : Type x}
{f : α → β → γ}
{s : Set α}
{t : Set β}
(hfs : ∀ b ∈ t, Set.InjOn (fun (x : α) => f x b) s)
(hft : ∀ a ∈ s, Set.InjOn (f a) t)
:
Set.Finite (Set.image2 f s t) ↔ Set.Finite s ∧ Set.Finite t ∨ s = ∅ ∨ t = ∅
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)
:
theorem
Set.infinite_range_of_injective
{α : Type u}
{β : Type v}
[Infinite α]
{f : α → β}
(hi : Function.Injective f)
:
theorem
Set.infinite_of_injective_forall_mem
{α : Type u}
{β : Type v}
[Infinite α]
{s : Set β}
{f : α → β}
(hi : Function.Injective f)
(hf : ∀ (x : α), f x ∈ s)
:
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))
:
Order properties #
theorem
Set.Infinite.exists_lt_map_eq_of_mapsTo
{α : Type u}
{β : Type v}
[LinearOrder α]
{s : Set α}
{t : Set β}
{f : α → β}
(hs : Set.Infinite s)
(hf : Set.MapsTo f s t)
(ht : Set.Finite t)
:
theorem
Set.Finite.exists_lt_map_eq_of_forall_mem
{α : Type u}
{β : Type v}
[LinearOrder α]
[Infinite α]
{t : Set β}
{f : α → β}
(hf : ∀ (a : α), f a ∈ t)
(ht : Set.Finite t)
:
theorem
Set.exists_min_image
{α : Type u}
{β : Type v}
[LinearOrder β]
(s : Set α)
(f : α → β)
(h1 : Set.Finite s)
:
Set.Nonempty s → ∃ a ∈ s, ∀ b ∈ s, f a ≤ f b
theorem
Set.exists_max_image
{α : Type u}
{β : Type v}
[LinearOrder β]
(s : Set α)
(f : α → β)
(h1 : Set.Finite s)
:
Set.Nonempty s → ∃ a ∈ s, ∀ b ∈ s, f b ≤ f a
theorem
Set.exists_lower_bound_image
{α : Type u}
{β : Type v}
[Nonempty α]
[LinearOrder β]
(s : Set α)
(f : α → β)
(h : Set.Finite s)
:
∃ (a : α), ∀ b ∈ s, f a ≤ f b
theorem
Set.exists_upper_bound_image
{α : Type u}
{β : Type v}
[Nonempty α]
[LinearOrder β]
(s : Set α)
(f : α → β)
(h : Set.Finite s)
:
∃ (a : α), ∀ b ∈ s, f b ≤ f a
theorem
Set.Finite.iSup_biInf_of_monotone
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[Preorder ι']
[Nonempty ι']
[IsDirected ι' fun (x x_1 : ι') => x ≤ x_1]
[Order.Frame α]
{s : Set ι}
(hs : Set.Finite s)
{f : ι → ι' → α}
(hf : ∀ i ∈ s, Monotone (f i))
:
⨆ (j : ι'), ⨅ i ∈ s, f i j = ⨅ i ∈ s, ⨆ (j : ι'), f i j
theorem
Set.Finite.iSup_biInf_of_antitone
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[Preorder ι']
[Nonempty ι']
[IsDirected ι' (Function.swap fun (x x_1 : ι') => x ≤ x_1)]
[Order.Frame α]
{s : Set ι}
(hs : Set.Finite s)
{f : ι → ι' → α}
(hf : ∀ i ∈ s, Antitone (f i))
:
⨆ (j : ι'), ⨅ i ∈ s, f i j = ⨅ i ∈ s, ⨆ (j : ι'), f i j
theorem
Set.Finite.iInf_biSup_of_monotone
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[Preorder ι']
[Nonempty ι']
[IsDirected ι' (Function.swap fun (x x_1 : ι') => x ≤ x_1)]
[Order.Coframe α]
{s : Set ι}
(hs : Set.Finite s)
{f : ι → ι' → α}
(hf : ∀ i ∈ s, Monotone (f i))
:
⨅ (j : ι'), ⨆ i ∈ s, f i j = ⨆ i ∈ s, ⨅ (j : ι'), f i j
theorem
Set.Finite.iInf_biSup_of_antitone
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[Preorder ι']
[Nonempty ι']
[IsDirected ι' fun (x x_1 : ι') => x ≤ x_1]
[Order.Coframe α]
{s : Set ι}
(hs : Set.Finite s)
{f : ι → ι' → α}
(hf : ∀ i ∈ s, Antitone (f i))
:
⨅ (j : ι'), ⨆ i ∈ s, f i j = ⨆ i ∈ s, ⨅ (j : ι'), f i j
theorem
Set.iSup_iInf_of_monotone
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[Finite ι]
[Preorder ι']
[Nonempty ι']
[IsDirected ι' fun (x x_1 : ι') => x ≤ x_1]
[Order.Frame α]
{f : ι → ι' → α}
(hf : ∀ (i : ι), Monotone (f i))
:
⨆ (j : ι'), ⨅ (i : ι), f i j = ⨅ (i : ι), ⨆ (j : ι'), f i j
theorem
Set.iSup_iInf_of_antitone
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[Finite ι]
[Preorder ι']
[Nonempty ι']
[IsDirected ι' (Function.swap fun (x x_1 : ι') => x ≤ x_1)]
[Order.Frame α]
{f : ι → ι' → α}
(hf : ∀ (i : ι), Antitone (f i))
:
⨆ (j : ι'), ⨅ (i : ι), f i j = ⨅ (i : ι), ⨆ (j : ι'), f i j
theorem
Set.iInf_iSup_of_monotone
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[Finite ι]
[Preorder ι']
[Nonempty ι']
[IsDirected ι' (Function.swap fun (x x_1 : ι') => x ≤ x_1)]
[Order.Coframe α]
{f : ι → ι' → α}
(hf : ∀ (i : ι), Monotone (f i))
:
⨅ (j : ι'), ⨆ (i : ι), f i j = ⨆ (i : ι), ⨅ (j : ι'), f i j
theorem
Set.iInf_iSup_of_antitone
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[Finite ι]
[Preorder ι']
[Nonempty ι']
[IsDirected ι' fun (x x_1 : ι') => x ≤ x_1]
[Order.Coframe α]
{f : ι → ι' → α}
(hf : ∀ (i : ι), Antitone (f i))
:
⨅ (j : ι'), ⨆ (i : ι), f i j = ⨆ (i : ι), ⨅ (j : ι'), f i j
theorem
Set.iUnion_iInter_of_monotone
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[Finite ι]
[Preorder ι']
[IsDirected ι' fun (x x_1 : ι') => x ≤ x_1]
[Nonempty ι']
{s : ι → ι' → Set α}
(hs : ∀ (i : ι), Monotone (s i))
:
⋃ (j : ι'), ⋂ (i : ι), s i j = ⋂ (i : ι), ⋃ (j : ι'), s i j
An increasing union distributes over finite intersection.
theorem
Set.iUnion_iInter_of_antitone
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[Finite ι]
[Preorder ι']
[IsDirected ι' (Function.swap fun (x x_1 : ι') => x ≤ x_1)]
[Nonempty ι']
{s : ι → ι' → Set α}
(hs : ∀ (i : ι), Antitone (s i))
:
⋃ (j : ι'), ⋂ (i : ι), s i j = ⋂ (i : ι), ⋃ (j : ι'), s i j
A decreasing union distributes over finite intersection.
theorem
Set.iInter_iUnion_of_monotone
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[Finite ι]
[Preorder ι']
[IsDirected ι' (Function.swap fun (x x_1 : ι') => x ≤ x_1)]
[Nonempty ι']
{s : ι → ι' → Set α}
(hs : ∀ (i : ι), Monotone (s i))
:
⋂ (j : ι'), ⋃ (i : ι), s i j = ⋃ (i : ι), ⋂ (j : ι'), s i j
An increasing intersection distributes over finite union.
theorem
Set.iInter_iUnion_of_antitone
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[Finite ι]
[Preorder ι']
[IsDirected ι' fun (x x_1 : ι') => x ≤ x_1]
[Nonempty ι']
{s : ι → ι' → Set α}
(hs : ∀ (i : ι), Antitone (s i))
:
⋂ (j : ι'), ⋃ (i : ι), s i j = ⋃ (i : ι), ⋂ (j : ι'), s i j
A decreasing intersection distributes over finite union.
theorem
Set.iUnion_pi_of_monotone
{ι : Type u_1}
{ι' : Type u_2}
[LinearOrder ι']
[Nonempty ι']
{α : ι → Type u_3}
{I : Set ι}
{s : (i : ι) → ι' → Set (α i)}
(hI : Set.Finite I)
(hs : ∀ i ∈ I, Monotone (s i))
:
theorem
Set.finite_range_findGreatest
{α : Type u}
{P : α → ℕ → Prop}
[(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}
[PartialOrder β]
(f : α → β)
(s : Set α)
(h : Set.Finite s)
(hs : Set.Nonempty s)
:
theorem
Set.Finite.exists_maximal_wrt'
{α : Type u}
{β : Type v}
[PartialOrder β]
(f : α → β)
(s : Set α)
(h : Set.Finite (f '' s))
(hs : Set.Nonempty s)
:
A version of Finite.exists_maximal_wrt with the (weaker) hypothesis that the image of s
is finite rather than s itself.
theorem
Set.Finite.exists_minimal_wrt
{α : Type u}
{β : Type v}
[PartialOrder β]
(f : α → β)
(s : Set α)
(h : Set.Finite s)
(hs : Set.Nonempty s)
:
theorem
Set.Finite.exists_minimal_wrt'
{α : Type u}
{β : Type v}
[PartialOrder β]
(f : α → β)
(s : Set α)
(h : Set.Finite (f '' s))
(hs : Set.Nonempty s)
:
A version of Finite.exists_minimal_wrt with the (weaker) hypothesis that the image of s
is finite rather than s itself.
theorem
Set.Finite.bddAbove
{α : Type u}
[Preorder α]
[IsDirected α fun (x x_1 : α) => x ≤ x_1]
[Nonempty α]
{s : Set α}
(hs : Set.Finite s)
:
BddAbove s
A finite set is bounded above.
theorem
Set.Finite.bddAbove_biUnion
{α : Type u}
{β : Type v}
[Preorder α]
[IsDirected α fun (x x_1 : α) => x ≤ x_1]
[Nonempty α]
{I : Set β}
{S : β → Set α}
(H : Set.Finite I)
:
A finite union of sets which are all bounded above is still bounded above.
theorem
Set.infinite_of_not_bddAbove
{α : Type u}
[Preorder α]
[IsDirected α fun (x x_1 : α) => x ≤ x_1]
[Nonempty α]
{s : Set α}
:
¬BddAbove s → Set.Infinite s
theorem
Set.Finite.bddBelow
{α : Type u}
[Preorder α]
[IsDirected α fun (x x_1 : α) => x ≥ x_1]
[Nonempty α]
{s : Set α}
(hs : Set.Finite s)
:
BddBelow s
A finite set is bounded below.
theorem
Set.Finite.bddBelow_biUnion
{α : Type u}
{β : Type v}
[Preorder α]
[IsDirected α fun (x x_1 : α) => x ≥ x_1]
[Nonempty α]
{I : Set β}
{S : β → Set α}
(H : Set.Finite I)
:
A finite union of sets which are all bounded below is still bounded below.
theorem
Set.infinite_of_not_bddBelow
{α : Type u}
[Preorder α]
[IsDirected α fun (x x_1 : α) => x ≥ x_1]
[Nonempty α]
{s : Set α}
:
¬BddBelow s → Set.Infinite s
A finset is bounded above.
A finset is bounded below.
theorem
Finite.of_forall_not_lt_lt
{α : Type u}
[LinearOrder α]
(h : ∀ ⦃x y z : α⦄, x < y → y < z → False)
:
Finite α
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}
[LinearOrder α]
{s : Set α}
(h : ∀ x ∈ s, ∀ y ∈ s, ∀ 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_iUnion_Ioo
{α : Type u}
[LinearOrder α]
(s : Set α)
:
Set.Finite (s \ ⋃ x ∈ s, ⋃ y ∈ s, Set.Ioo x y)
theorem
Set.finite_diff_iUnion_Ioo'
{α : Type u}
[LinearOrder α]
(s : Set α)
:
Set.Finite (s \ ⋃ (x : ↑s × ↑s), Set.Ioo ↑x.1 ↑x.2)