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 #

Implementation #

A finite set is defined to be a set whose coercion to a type has a Finite instance.

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

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

A set is finite if the corresponding Subtype is finite, i.e., if there exists a natural n : ℕ and an equivalence s ≃ Fin n.

Equations
Instances For
    theorem Set.finite_def {α : Type u} {s : Set α} :
    s.Finite Nonempty (Fintype s)
    theorem Set.Finite.nonempty_fintype {α : Type u} {s : Set α} :
    s.FiniteNonempty (Fintype s)

    Alias of the forward direction of Set.finite_def.

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

    Constructor for Set.Finite using a Finite instance.

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

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

    theorem Set.Finite.to_subtype {α : Type u} {s : Set α} (h : s.Finite) :
    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 : s.Finite) :
    Fintype 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
    • h.fintype = .some
    Instances For
      noncomputable def Set.Finite.toFinset {α : Type u} {s : Set α} (h : s.Finite) :

      Using choice, get the Finset that represents this Set.

      Equations
      • h.toFinset = s.toFinset
      Instances For
        theorem Set.Finite.toFinset_eq_toFinset {α : Type u} {s : Set α} [Fintype s] (h : s.Finite) :
        h.toFinset = s.toFinset
        @[simp]
        theorem Set.toFinite_toFinset {α : Type u} (s : Set α) [Fintype s] :
        .toFinset = s.toFinset
        theorem Set.Finite.exists_finset {α : Type u} {s : Set α} (h : s.Finite) :
        ∃ (s' : Finset α), ∀ (a : α), a s' a s
        theorem Set.Finite.exists_finset_coe {α : Type u} {s : Set α} (h : s.Finite) :
        ∃ (s' : Finset α), s' = s
        instance Set.instCanLiftFinsetToSetFinite {α : Type u} :
        CanLift (Set α) (Finset α) Finset.toSet Set.Finite

        Finite sets can be lifted to finsets.

        Equations
        • =
        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
        • s.Infinite = ¬s.Finite
        Instances For
          @[simp]
          theorem Set.not_infinite {α : Type u} {s : Set α} :
          ¬s.Infinite s.Finite
          @[simp]
          theorem Set.Finite.not_infinite {α : Type u} {s : Set α} :
          s.Finite¬s.Infinite

          Alias of the reverse direction of Set.not_infinite.

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

          See also finite_or_infinite, fintypeOrInfinite.

          theorem Set.infinite_or_finite {α : Type u} (s : Set α) :
          s.Infinite s.Finite

          Basic properties of Set.Finite.toFinset #

          @[simp]
          theorem Set.Finite.mem_toFinset {α : Type u} {s : Set α} {a : α} (hs : s.Finite) :
          a hs.toFinset a s
          @[simp]
          theorem Set.Finite.coe_toFinset {α : Type u} {s : Set α} (hs : s.Finite) :
          hs.toFinset = s
          @[simp]
          theorem Set.Finite.toFinset_nonempty {α : Type u} {s : Set α} (hs : s.Finite) :
          hs.toFinset.Nonempty s.Nonempty
          theorem Set.Finite.coeSort_toFinset {α : Type u} {s : Set α} (hs : s.Finite) :
          { x : α // x hs.toFinset } = 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 : s.Finite) (b : { b : α // (fun (x : α) => x hs.toFinset) b }) :
          (hs.subtypeEquivToFinset.symm b) = b
          @[simp]
          theorem Set.Finite.subtypeEquivToFinset_apply_coe {α : Type u} {s : Set α} (hs : s.Finite) (a : { a : α // (fun (x : α) => x s) a }) :
          (hs.subtypeEquivToFinset a) = a
          def Set.Finite.subtypeEquivToFinset {α : Type u} {s : Set α} (hs : s.Finite) :
          { x : α // x s } { x : α // x hs.toFinset }

          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
          • hs.subtypeEquivToFinset = (Equiv.refl α).subtypeEquiv
          Instances For
            @[simp]
            theorem Set.Finite.toFinset_inj {α : Type u} {s : Set α} {t : Set α} {hs : s.Finite} {ht : t.Finite} :
            hs.toFinset = ht.toFinset s = t
            @[simp]
            theorem Set.Finite.toFinset_subset {α : Type u} {s : Set α} {hs : s.Finite} {t : Finset α} :
            hs.toFinset t s t
            @[simp]
            theorem Set.Finite.toFinset_ssubset {α : Type u} {s : Set α} {hs : s.Finite} {t : Finset α} :
            hs.toFinset t s t
            @[simp]
            theorem Set.Finite.subset_toFinset {α : Type u} {t : Set α} {ht : t.Finite} {s : Finset α} :
            s ht.toFinset s t
            @[simp]
            theorem Set.Finite.ssubset_toFinset {α : Type u} {t : Set α} {ht : t.Finite} {s : Finset α} :
            s ht.toFinset s t
            theorem Set.Finite.toFinset_subset_toFinset {α : Type u} {s : Set α} {t : Set α} {hs : s.Finite} {ht : t.Finite} :
            hs.toFinset ht.toFinset s t
            theorem Set.Finite.toFinset_ssubset_toFinset {α : Type u} {s : Set α} {t : Set α} {hs : s.Finite} {ht : t.Finite} :
            hs.toFinset ht.toFinset s t
            theorem Set.Finite.toFinset_mono {α : Type u} {s : Set α} {t : Set α} {hs : s.Finite} {ht : t.Finite} :
            s ths.toFinset ht.toFinset

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

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

            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 : {x : α | p x}.Finite) :
            h.toFinset = Finset.filter p Finset.univ
            @[simp]
            theorem Set.Finite.disjoint_toFinset {α : Type u} {s : Set α} {t : Set α} {hs : s.Finite} {ht : t.Finite} :
            Disjoint hs.toFinset ht.toFinset Disjoint s t
            theorem Set.Finite.toFinset_inter {α : Type u} {s : Set α} {t : Set α} [DecidableEq α] (hs : s.Finite) (ht : t.Finite) (h : (s t).Finite) :
            h.toFinset = hs.toFinset ht.toFinset
            theorem Set.Finite.toFinset_union {α : Type u} {s : Set α} {t : Set α} [DecidableEq α] (hs : s.Finite) (ht : t.Finite) (h : (s t).Finite) :
            h.toFinset = hs.toFinset ht.toFinset
            theorem Set.Finite.toFinset_diff {α : Type u} {s : Set α} {t : Set α} [DecidableEq α] (hs : s.Finite) (ht : t.Finite) (h : (s \ t).Finite) :
            h.toFinset = hs.toFinset \ ht.toFinset
            theorem Set.Finite.toFinset_symmDiff {α : Type u} {s : Set α} {t : Set α} [DecidableEq α] (hs : s.Finite) (ht : t.Finite) (h : (symmDiff s t).Finite) :
            h.toFinset = symmDiff hs.toFinset ht.toFinset
            theorem Set.Finite.toFinset_compl {α : Type u} {s : Set α} [DecidableEq α] [Fintype α] (hs : s.Finite) (h : s.Finite) :
            h.toFinset = hs.toFinset
            theorem Set.Finite.toFinset_univ {α : Type u} [Fintype α] (h : Set.univ.Finite) :
            h.toFinset = Finset.univ
            @[simp]
            theorem Set.Finite.toFinset_eq_empty {α : Type u} {s : Set α} {h : s.Finite} :
            h.toFinset = s =
            theorem Set.Finite.toFinset_empty {α : Type u} (h : .Finite) :
            h.toFinset =
            @[simp]
            theorem Set.Finite.toFinset_eq_univ {α : Type u} {s : Set α} [Fintype α] {h : s.Finite} :
            h.toFinset = Finset.univ s = Set.univ
            theorem Set.Finite.toFinset_image {α : Type u} {β : Type v} {s : Set α} [DecidableEq β] (f : αβ) (hs : s.Finite) (h : (f '' s).Finite) :
            h.toFinset = Finset.image f hs.toFinset
            theorem Set.Finite.toFinset_range {α : Type u} {β : Type v} [DecidableEq α] [Fintype β] (f : βα) (h : (Set.range f).Finite) :
            h.toFinset = 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} [Fintype α] :
            Fintype Set.univ
            Equations
            noncomputable def Set.fintypeOfFiniteUniv {α : Type u} (H : Set.univ.Finite) :

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

            Equations
            Instances For
              instance Set.fintypeUnion {α : Type u} [DecidableEq α] (s : Set α) (t : Set α) [Fintype s] [Fintype t] :
              Fintype (s t)
              Equations
              instance Set.fintypeSep {α : Type u} (s : Set α) (p : αProp) [Fintype s] [DecidablePred p] :
              Fintype {a : α | a s p a}
              Equations
              instance Set.fintypeInter {α : Type u} (s : Set α) (t : Set α) [DecidableEq α] [Fintype s] [Fintype t] :
              Fintype (s t)
              Equations
              instance Set.fintypeInterOfLeft {α : Type u} (s : Set α) (t : Set α) [Fintype s] [DecidablePred fun (x : α) => x t] :
              Fintype (s t)

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

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

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

              Equations
              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
              • s.fintypeSubset h = .mpr (s.fintypeInterOfLeft t)
              Instances For
                instance Set.fintypeDiff {α : Type u} [DecidableEq α] (s : Set α) (t : Set α) [Fintype s] [Fintype t] :
                Fintype (s \ t)
                Equations
                instance Set.fintypeDiffLeft {α : Type u} (s : Set α) (t : Set α) [Fintype s] [DecidablePred fun (x : α) => x t] :
                Fintype (s \ t)
                Equations
                • s.fintypeDiffLeft t = s.fintypeSep 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
                instance Set.fintypesUnion {α : Type u} [DecidableEq α] {s : Set (Set α)} [Fintype s] [H : (t : s) → Fintype t] :
                Equations
                def Set.fintypeBiUnion {α : Type u} [DecidableEq α] {ι : Type u_1} (s : Set ι) [Fintype s] (t : ιSet α) (H : (i : ι) → i sFintype (t i)) :
                Fintype (xs, t x)

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

                Equations
                • s.fintypeBiUnion t H = Fintype.ofFinset (s.toFinset.attach.biUnion fun (x : { x : ι // x s.toFinset }) => (t x).toFinset)
                Instances For
                  instance Set.fintypeBiUnion' {α : Type u} [DecidableEq α] {ι : Type u_1} (s : Set ι) [Fintype s] (t : ιSet α) [(i : ι) → Fintype (t i)] :
                  Fintype (xs, t x)
                  Equations
                  • s.fintypeBiUnion' t = Fintype.ofFinset (s.toFinset.biUnion fun (x : ι) => (t x).toFinset)
                  theorem Set.toFinset_iUnion {α : Type u} {β : Type v} [Fintype β] [DecidableEq α] (f : βSet α) [(w : β) → Fintype (f w)] :
                  (⋃ (x : β), f x).toFinset = Finset.univ.biUnion fun (x : β) => (f x).toFinset
                  def Set.fintypeBind {α : Type u_1} {β : Type u_1} [DecidableEq β] (s : Set α) [Fintype s] (f : αSet β) (H : (a : α) → a sFintype (f a)) :
                  Fintype (s >>= f)

                  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
                  • s.fintypeBind f H = s.fintypeBiUnion f H
                  Instances For
                    instance Set.fintypeBind' {α : Type u_1} {β : Type u_1} [DecidableEq β] (s : Set α) [Fintype s] (f : αSet β) [(a : α) → Fintype (f a)] :
                    Fintype (s >>= f)
                    Equations
                    • s.fintypeBind' f = s.fintypeBiUnion' f
                    instance Set.fintypeEmpty {α : Type u} :
                    Equations
                    instance Set.fintypeSingleton {α : Type u} (a : α) :
                    Fintype {a}
                    Equations
                    instance Set.fintypePure {α : Type u} (a : α) :
                    Fintype (pure a)
                    Equations
                    • Set.fintypePure = Set.fintypeSingleton
                    instance Set.fintypeInsert {α : Type u} (a : α) (s : Set α) [DecidableEq α] [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 is decidable.

                    Equations
                    def Set.fintypeInsertOfNotMem {α : Type u} {a : α} (s : Set α) [Fintype s] (h : as) :
                    Fintype (insert a s)

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

                    Equations
                    Instances For
                      def Set.fintypeInsertOfMem {α : Type u} {a : α} (s : Set α) [Fintype s] (h : a s) :
                      Fintype (insert a s)

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

                      Equations
                      Instances For
                        @[instance 100]
                        instance Set.fintypeInsert' {α : Type u} (a : α) (s : Set α) [Decidable (a s)] [Fintype s] :
                        Fintype (insert a s)

                        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
                        instance Set.fintypeImage {α : Type u} {β : Type v} [DecidableEq β] (s : Set α) (f : αβ) [Fintype s] :
                        Fintype (f '' s)
                        Equations
                        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
                        Instances For
                          instance Set.fintypeRange {α : Type u} {ι : Sort w} [DecidableEq α] (f : ια) [Fintype (PLift ι)] :
                          Equations
                          instance Set.fintypeMap {α : Type u_1} {β : Type u_1} [DecidableEq β] (s : Set α) (f : αβ) [Fintype s] :
                          Fintype (f <$> s)
                          Equations
                          • Set.fintypeMap = Set.fintypeImage
                          instance Set.fintypeLTNat (n : ) :
                          Fintype {i : | i < n}
                          Equations
                          instance Set.fintypeLENat (n : ) :
                          Fintype {i : | i n}
                          Equations

                          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] :
                            Fintype (s ×ˢ t)
                            Equations
                            instance Set.fintypeOffDiag {α : Type u} [DecidableEq α] (s : Set α) [Fintype s] :
                            Fintype s.offDiag
                            Equations
                            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
                            instance Set.fintypeSeq {α : Type u} {β : Type v} [DecidableEq β] (f : Set (αβ)) (s : Set α) [Fintype f] [Fintype s] :
                            Fintype (f.seq s)
                            Equations
                            • f.fintypeSeq s = .mpr (f.fintypeBiUnion' fun (x : αβ) => x '' s)
                            instance Set.fintypeSeq' {α : Type u} {β : Type u} [DecidableEq β] (f : Set (αβ)) (s : Set α) [Fintype f] [Fintype s] :
                            Fintype (Seq.seq f fun (x : Unit) => s)
                            Equations
                            • f.fintypeSeq' s = f.fintypeSeq s
                            instance Set.fintypeMemFinset {α : Type u} (s : Finset α) :
                            Fintype {a : α | a s}
                            Equations
                            theorem Equiv.set_finite_iff {α : Type u} {β : Type v} {s : Set α} {t : Set β} (hst : s t) :
                            s.Finite t.Finite

                            Finset #

                            @[simp]
                            theorem Finset.finite_toSet {α : Type u} (s : Finset α) :
                            (s).Finite

                            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 α) :
                            .toFinset = s
                            @[simp]
                            theorem Multiset.finite_toSet {α : Type u} (s : Multiset α) :
                            {x : α | x s}.Finite
                            @[simp]
                            theorem Multiset.finite_toSet_toFinset {α : Type u} [DecidableEq α] (s : Multiset α) :
                            .toFinset = s.toFinset
                            @[simp]
                            theorem List.finite_toSet {α : Type u} (l : List α) :
                            {x : α | x l}.Finite

                            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 α) [Finite s] [Finite t] :
                            Finite (s t)
                            Equations
                            • =
                            instance Finite.Set.finite_sep {α : Type u} (s : Set α) (p : αProp) [Finite s] :
                            Finite {a : α | a s p a}
                            Equations
                            • =
                            theorem Finite.Set.subset {α : Type u} (s : Set α) {t : Set α} [Finite s] (h : t s) :
                            Finite t
                            instance Finite.Set.finite_inter_of_right {α : Type u} (s : Set α) (t : Set α) [Finite t] :
                            Finite (s t)
                            Equations
                            • =
                            instance Finite.Set.finite_inter_of_left {α : Type u} (s : Set α) (t : Set α) [Finite s] :
                            Finite (s t)
                            Equations
                            • =
                            instance Finite.Set.finite_diff {α : Type u} (s : Set α) (t : Set α) [Finite s] :
                            Finite (s \ t)
                            Equations
                            • =
                            instance Finite.Set.finite_range {α : Type u} {ι : Sort w} (f : ια) [Finite ι] :
                            Equations
                            • =
                            instance Finite.Set.finite_iUnion {α : Type u} {ι : Sort w} [Finite ι] (f : ιSet α) [∀ (i : ι), Finite (f i)] :
                            Finite (⋃ (i : ι), f i)
                            Equations
                            • =
                            instance Finite.Set.finite_sUnion {α : Type u} {s : Set (Set α)} [Finite s] [H : ∀ (t : s), Finite t] :
                            Finite (⋃₀ s)
                            Equations
                            • =
                            theorem Finite.Set.finite_biUnion {α : Type u} {ι : Type u_1} (s : Set ι) [Finite s] (t : ιSet α) (H : is, Finite (t i)) :
                            Finite (xs, t x)
                            instance Finite.Set.finite_biUnion' {α : Type u} {ι : Type u_1} (s : Set ι) [Finite s] (t : ιSet α) [∀ (i : ι), Finite (t i)] :
                            Finite (xs, t x)
                            Equations
                            • =
                            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 Order.Interval.Finset.Nat).

                            Equations
                            • =
                            instance Finite.Set.finite_iInter {α : Type u} {ι : Sort u_1} [Nonempty ι] (t : ιSet α) [∀ (i : ι), Finite (t i)] :
                            Finite (⋂ (i : ι), t i)
                            Equations
                            • =
                            instance Finite.Set.finite_insert {α : Type u} (a : α) (s : Set α) [Finite s] :
                            Finite (insert a s)
                            Equations
                            • =
                            instance Finite.Set.finite_image {α : Type u} {β : Type v} (s : Set α) (f : αβ) [Finite s] :
                            Finite (f '' s)
                            Equations
                            • =
                            instance Finite.Set.finite_replacement {α : Type u} {β : Type v} [Finite α] (f : αβ) :
                            Finite {x : β | ∃ (x_1 : α), f x_1 = x}
                            Equations
                            • =
                            instance Finite.Set.finite_prod {α : Type u} {β : Type v} (s : Set α) (t : Set β) [Finite s] [Finite t] :
                            Finite (s ×ˢ t)
                            Equations
                            • =
                            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
                            • =
                            instance Finite.Set.finite_seq {α : Type u} {β : Type v} (f : Set (αβ)) (s : Set α) [Finite f] [Finite s] :
                            Finite (f.seq s)
                            Equations
                            • =

                            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} [Subsingleton α] (s : Set α) :
                            s.Finite
                            theorem Set.finite_univ {α : Type u} [Finite α] :
                            Set.univ.Finite
                            theorem Set.finite_univ_iff {α : Type u} :
                            Set.univ.Finite Finite α
                            theorem Finite.of_finite_univ {α : Type u} :
                            Set.univ.FiniteFinite α

                            Alias of the forward direction of Set.finite_univ_iff.

                            theorem Set.Finite.subset {α : Type u} {s : Set α} (hs : s.Finite) {t : Set α} (ht : t s) :
                            t.Finite
                            theorem Set.Finite.union {α : Type u} {s : Set α} {t : Set α} (hs : s.Finite) (ht : t.Finite) :
                            (s t).Finite
                            theorem Set.Finite.finite_of_compl {α : Type u} {s : Set α} (hs : s.Finite) (hsc : s.Finite) :
                            theorem Set.Finite.sup {α : Type u} {s : Set α} {t : Set α} :
                            s.Finitet.Finite(s t).Finite
                            theorem Set.Finite.sep {α : Type u} {s : Set α} (hs : s.Finite) (p : αProp) :
                            {a : α | a s p a}.Finite
                            theorem Set.Finite.inter_of_left {α : Type u} {s : Set α} (hs : s.Finite) (t : Set α) :
                            (s t).Finite
                            theorem Set.Finite.inter_of_right {α : Type u} {s : Set α} (hs : s.Finite) (t : Set α) :
                            (t s).Finite
                            theorem Set.Finite.inf_of_left {α : Type u} {s : Set α} (h : s.Finite) (t : Set α) :
                            (s t).Finite
                            theorem Set.Finite.inf_of_right {α : Type u} {s : Set α} (h : s.Finite) (t : Set α) :
                            (t s).Finite
                            theorem Set.Infinite.mono {α : Type u} {s : Set α} {t : Set α} (h : s t) :
                            s.Infinitet.Infinite
                            theorem Set.Finite.diff {α : Type u} {s : Set α} (hs : s.Finite) (t : Set α) :
                            (s \ t).Finite
                            theorem Set.Finite.of_diff {α : Type u} {s : Set α} {t : Set α} (hd : (s \ t).Finite) (ht : t.Finite) :
                            s.Finite
                            theorem Set.finite_iUnion {α : Type u} {ι : Sort w} [Finite ι] {f : ιSet α} (H : ∀ (i : ι), (f i).Finite) :
                            (⋃ (i : ι), f i).Finite
                            theorem Set.Finite.biUnion' {α : Type u} {ι : Type u_1} {s : Set ι} (hs : s.Finite) {t : (i : ι) → i sSet α} (ht : ∀ (i : ι) (hi : i s), (t i hi).Finite) :
                            (⋃ (i : ι), ⋃ (h : i s), t i h).Finite

                            Dependent version of Finite.biUnion.

                            theorem Set.Finite.biUnion {α : Type u} {ι : Type u_1} {s : Set ι} (hs : s.Finite) {t : ιSet α} (ht : is, (t i).Finite) :
                            (is, t i).Finite
                            theorem Set.Finite.sUnion {α : Type u} {s : Set (Set α)} (hs : s.Finite) (H : ts, t.Finite) :
                            (⋃₀ s).Finite
                            theorem Set.Finite.sInter {α : Type u_1} {s : Set (Set α)} {t : Set α} (ht : t s) (hf : t.Finite) :
                            (⋂₀ s).Finite
                            theorem Set.Finite.iUnion {α : Type u} {ι : Type u_1} {s : ιSet α} {t : Set ι} (ht : t.Finite) (hs : it, (s i).Finite) (he : it, s i = ) :
                            (⋃ (i : ι), s i).Finite

                            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 : s.Finite) (hf : as, (f a).Finite) :
                            (s >>= f).Finite
                            @[simp]
                            theorem Set.finite_empty {α : Type u} :
                            .Finite
                            theorem Set.Infinite.nonempty {α : Type u} {s : Set α} (h : s.Infinite) :
                            s.Nonempty
                            @[simp]
                            theorem Set.finite_singleton {α : Type u} (a : α) :
                            {a}.Finite
                            theorem Set.finite_pure {α : Type u} (a : α) :
                            (pure a).Finite
                            @[simp]
                            theorem Set.Finite.insert {α : Type u} (a : α) {s : Set α} (hs : s.Finite) :
                            (insert a s).Finite
                            theorem Set.Finite.image {α : Type u} {β : Type v} {s : Set α} (f : αβ) (hs : s.Finite) :
                            (f '' s).Finite
                            theorem Set.finite_range {α : Type u} {ι : Sort w} (f : ια) [Finite ι] :
                            (Set.range f).Finite
                            theorem Set.Finite.of_surjOn {α : Type u} {β : Type v} {s : Set α} {t : Set β} (f : αβ) (hf : Set.SurjOn f s t) (hs : s.Finite) :
                            t.Finite
                            theorem Set.Finite.dependent_image {α : Type u} {β : Type v} {s : Set α} (hs : s.Finite) (F : (i : α) → i sβ) :
                            {y : β | ∃ (x : α) (hx : x s), F x hx = y}.Finite
                            theorem Set.Finite.map {α : Type u_1} {β : Type u_1} {s : Set α} (f : αβ) :
                            s.Finite(f <$> s).Finite
                            theorem Set.Finite.of_finite_image {α : Type u} {β : Type v} {s : Set α} {f : αβ} (h : (f '' s).Finite) (hi : Set.InjOn f s) :
                            s.Finite
                            theorem Set.finite_of_finite_preimage {α : Type u} {β : Type v} {f : αβ} {s : Set β} (h : (f ⁻¹' s).Finite) (hs : s Set.range f) :
                            s.Finite
                            theorem Set.Finite.of_preimage {α : Type u} {β : Type v} {f : αβ} {s : Set β} (h : (f ⁻¹' s).Finite) (hf : Function.Surjective f) :
                            s.Finite
                            theorem Set.Finite.preimage {α : Type u} {β : Type v} {f : αβ} {s : Set β} (I : Set.InjOn f (f ⁻¹' s)) (h : s.Finite) :
                            (f ⁻¹' s).Finite
                            theorem Set.Finite.preimage' {α : Type u} {β : Type v} {f : αβ} {s : Set β} (h : s.Finite) (hf : bs, (f ⁻¹' {b}).Finite) :
                            (f ⁻¹' s).Finite
                            theorem Set.Infinite.preimage {α : Type u} {β : Type v} {f : αβ} {s : Set β} (hs : s.Infinite) (hf : s Set.range f) :
                            (f ⁻¹' s).Infinite
                            theorem Set.Infinite.preimage' {α : Type u} {β : Type v} {f : αβ} {s : Set β} (hs : (s Set.range f).Infinite) :
                            (f ⁻¹' s).Infinite
                            theorem Set.Finite.preimage_embedding {α : Type u} {β : Type v} {s : Set β} (f : α β) (h : s.Finite) :
                            (f ⁻¹' s).Finite
                            theorem Set.finite_lt_nat (n : ) :
                            {i : | i < n}.Finite
                            theorem Set.finite_le_nat (n : ) :
                            {i : | i n}.Finite
                            theorem Set.Finite.surjOn_iff_bijOn_of_mapsTo {α : Type u} {s : Set α} {f : αα} (hs : s.Finite) (hm : Set.MapsTo f s s) :
                            theorem Set.Finite.injOn_iff_bijOn_of_mapsTo {α : Type u} {s : Set α} {f : αα} (hs : s.Finite) (hm : Set.MapsTo f s s) :
                            theorem Set.Finite.prod {α : Type u} {β : Type v} {s : Set α} {t : Set β} (hs : s.Finite) (ht : t.Finite) :
                            (s ×ˢ t).Finite
                            theorem Set.Finite.of_prod_left {α : Type u} {β : Type v} {s : Set α} {t : Set β} (h : (s ×ˢ t).Finite) :
                            t.Nonemptys.Finite
                            theorem Set.Finite.of_prod_right {α : Type u} {β : Type v} {s : Set α} {t : Set β} (h : (s ×ˢ t).Finite) :
                            s.Nonemptyt.Finite
                            theorem Set.Infinite.prod_left {α : Type u} {β : Type v} {s : Set α} {t : Set β} (hs : s.Infinite) (ht : t.Nonempty) :
                            (s ×ˢ t).Infinite
                            theorem Set.Infinite.prod_right {α : Type u} {β : Type v} {s : Set α} {t : Set β} (ht : t.Infinite) (hs : s.Nonempty) :
                            (s ×ˢ t).Infinite
                            theorem Set.infinite_prod {α : Type u} {β : Type v} {s : Set α} {t : Set β} :
                            (s ×ˢ t).Infinite s.Infinite t.Nonempty t.Infinite s.Nonempty
                            theorem Set.finite_prod {α : Type u} {β : Type v} {s : Set α} {t : Set β} :
                            (s ×ˢ t).Finite (s.Finite t = ) (t.Finite s = )
                            theorem Set.Finite.offDiag {α : Type u} {s : Set α} (hs : s.Finite) :
                            s.offDiag.Finite
                            theorem Set.Finite.image2 {α : Type u} {β : Type v} {γ : Type x} {s : Set α} {t : Set β} (f : αβγ) (hs : s.Finite) (ht : t.Finite) :
                            (Set.image2 f s t).Finite
                            theorem Set.Finite.seq {α : Type u} {β : Type v} {f : Set (αβ)} {s : Set α} (hf : f.Finite) (hs : s.Finite) :
                            (f.seq s).Finite
                            theorem Set.Finite.seq' {α : Type u} {β : Type u} {f : Set (αβ)} {s : Set α} (hf : f.Finite) (hs : s.Finite) :
                            (Seq.seq f fun (x : Unit) => s).Finite
                            theorem Set.finite_mem_finset {α : Type u} (s : Finset α) :
                            {a : α | a s}.Finite
                            theorem Set.Subsingleton.finite {α : Type u} {s : Set α} (h : s.Subsingleton) :
                            s.Finite
                            theorem Set.Infinite.nontrivial {α : Type u} {s : Set α} (hs : s.Infinite) :
                            s.Nontrivial
                            theorem Set.finite_preimage_inl_and_inr {α : Type u} {β : Type v} {s : Set (α β)} :
                            (Sum.inl ⁻¹' s).Finite (Sum.inr ⁻¹' s).Finite s.Finite
                            theorem Set.exists_finite_iff_finset {α : Type u} {p : Set αProp} :
                            (∃ (s : Set α), s.Finite p s) ∃ (s : Finset α), p s
                            theorem Set.Finite.finite_subsets {α : Type u} {a : Set α} (h : a.Finite) :
                            {b : Set α | b a}.Finite

                            There are finitely many subsets of a given finite set

                            theorem Set.Finite.powerset {α : Type u} {s : Set α} (h : s.Finite) :
                            (𝒫 s).Finite
                            theorem Set.exists_subset_image_finite_and {α : Type u} {β : Type v} {f : αβ} {s : Set α} {p : Set βProp} :
                            (tf '' s, t.Finite p t) ts, t.Finite p (f '' t)
                            theorem Set.Finite.pi {ι : Type u_1} [Finite ι] {κ : ιType u_2} {t : (i : ι) → Set (κ i)} (ht : ∀ (i : ι), (t i).Finite) :
                            (Set.univ.pi t).Finite

                            Finite product of finite sets is finite

                            theorem Set.Finite.pi' {ι : Type u_1} [Finite ι] {κ : ιType u_2} {t : (i : ι) → Set (κ i)} (ht : ∀ (i : ι), (t i).Finite) :
                            {f : (i : ι) → κ i | ∀ (i : ι), f i t i}.Finite

                            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.range f).Finite) :
                            (⋃ (a : α), (f a)).Finite

                            A finite union of finsets is finite.

                            theorem Set.finite_range_ite {α : Type u} {β : Type v} {p : αProp} [DecidablePred p] {f : αβ} {g : αβ} (hf : (Set.range f).Finite) (hg : (Set.range g).Finite) :
                            (Set.range fun (x : α) => if p x then f x else g x).Finite
                            theorem Set.finite_range_const {α : Type u} {β : Type v} {c : β} :
                            (Set.range fun (x : α) => c).Finite

                            Properties #

                            instance Set.Finite.inhabited {α : Type u} :
                            Inhabited { s : Set α // s.Finite }
                            Equations
                            • Set.Finite.inhabited = { default := , }
                            @[simp]
                            theorem Set.finite_union {α : Type u} {s : Set α} {t : Set α} :
                            (s t).Finite s.Finite t.Finite
                            theorem Set.finite_image_iff {α : Type u} {β : Type v} {s : Set α} {f : αβ} (hi : Set.InjOn f s) :
                            (f '' s).Finite s.Finite
                            theorem Set.univ_finite_iff_nonempty_fintype {α : Type u} :
                            Set.univ.Finite Nonempty (Fintype α)
                            theorem Set.Finite.toFinset_singleton {α : Type u} {a : α} (ha : optParam {a}.Finite ) :
                            @[simp]
                            theorem Set.Finite.toFinset_insert {α : Type u} [DecidableEq α] {s : Set α} {a : α} (hs : (insert a s).Finite) :
                            hs.toFinset = insert a .toFinset
                            theorem Set.Finite.toFinset_insert' {α : Type u} [DecidableEq α] {a : α} {s : Set α} (hs : s.Finite) :
                            .toFinset = insert a hs.toFinset
                            theorem Set.Finite.toFinset_prod {α : Type u} {β : Type v} {s : Set α} {t : Set β} (hs : s.Finite) (ht : t.Finite) :
                            hs.toFinset ×ˢ ht.toFinset = .toFinset
                            theorem Set.Finite.toFinset_offDiag {α : Type u} {s : Set α} [DecidableEq α] (hs : s.Finite) :
                            .toFinset = hs.toFinset.offDiag
                            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_option {α : Type u} {s : Set (Option α)} :
                            s.Finite {x : α | some x s}.Finite
                            theorem Set.finite_image_fst_and_snd_iff {α : Type u} {β : Type v} {s : Set (α × β)} :
                            (Prod.fst '' s).Finite (Prod.snd '' s).Finite s.Finite
                            theorem Set.forall_finite_image_eval_iff {δ : Type u_1} [Finite δ] {κ : δType u_2} {s : Set ((d : δ) → κ d)} :
                            (∀ (d : δ), (Function.eval d '' s).Finite) s.Finite
                            theorem Set.finite_subset_iUnion {α : Type u} {s : Set α} (hs : s.Finite) {ι : Type u_1} {t : ιSet α} (h : s ⋃ (i : ι), t i) :
                            ∃ (I : Set ι), I.Finite s iI, t i
                            theorem Set.eq_finite_iUnion_of_finite_subset_iUnion {α : Type u} {ι : Type u_1} {s : ιSet α} {t : Set α} (tfin : t.Finite) (h : t ⋃ (i : ι), s i) :
                            ∃ (I : Set ι), I.Finite ∃ (σ : {i : ι | i I}Set α), (∀ (i : {i : ι | i I}), (σ i).Finite) (∀ (i : {i : ι | i I}), σ i s i) t = ⋃ (i : {i : ι | i I}), σ i
                            theorem Set.Finite.induction_on {α : Type u} {C : Set αProp} {s : Set α} (h : s.Finite) (H0 : C ) (H1 : ∀ {a : α} {s : Set α}, ass.FiniteC sC (insert a s)) :
                            C s
                            theorem Set.Finite.induction_on' {α : Type u} {C : Set αProp} {S : Set α} (h : S.Finite) (H0 : C ) (H1 : ∀ {a : α} {s : Set α}, a Ss SasC sC (insert a s)) :
                            C S

                            Analogous to Finset.induction_on'.

                            theorem Set.Finite.dinduction_on {α : Type u} {C : (s : Set α) → s.FiniteProp} (s : Set α) (h : s.Finite) (H0 : C ) (H1 : ∀ {a : α} {s : Set α}, as∀ (h : s.Finite), C s hC (insert a s) ) :
                            C s h
                            theorem Set.Finite.induction_to {α : Type u} {C : Set αProp} {S : Set α} (h : S.Finite) (S0 : Set α) (hS0 : S0 S) (H0 : C S0) (H1 : sS, C saS \ 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.univC SaS, C (insert a S)) :
                            C Set.univ

                            Induction up to univ.

                            theorem Set.seq_of_forall_finite_exists {γ : Type u_1} {P : γSet γProp} (h : ∀ (t : Set γ), t.Finite∃ (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} :
                            theorem Set.empty_card' {α : Type u} {h : Fintype } :
                            theorem Set.card_fintypeInsertOfNotMem {α : Type u} {a : α} (s : Set α) [Fintype s] (h : as) :
                            @[simp]
                            theorem Set.card_insert {α : Type u} {a : α} (s : Set α) [Fintype s] (h : as) {d : Fintype (insert a s)} :
                            theorem Set.card_image_of_inj_on {α : Type u} {β : Type v} {s : Set α} [Fintype s] {f : αβ} [Fintype (f '' s)] (H : xs, ys, f x = f yx = y) :
                            theorem Set.card_image_of_injective {α : Type u} {β : Type v} (s : Set α) [Fintype s] {f : αβ} [Fintype (f '' s)] (H : Function.Injective f) :
                            @[simp]
                            theorem Set.card_singleton {α : Type u} (a : α) :
                            Fintype.card {a} = 1
                            theorem Set.card_lt_card {α : Type u} {s : Set α} {t : Set α} [Fintype s] [Fintype t] (h : s t) :
                            theorem Set.card_le_card {α : Type u} {s : Set α} {t : Set α} [Fintype s] [Fintype t] (hsub : s 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)] :
                            theorem Set.Finite.card_toFinset {α : Type u} {s : Set α} [Fintype s] (h : s.Finite) :
                            h.toFinset.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 #

                            theorem Set.infinite_univ_iff {α : Type u} :
                            Set.univ.Infinite Infinite α
                            theorem Set.infinite_univ {α : Type u} [h : Infinite α] :
                            Set.univ.Infinite
                            theorem Set.infinite_coe_iff {α : Type u} {s : Set α} :
                            Infinite s s.Infinite
                            theorem Set.Infinite.to_subtype {α : Type u} {s : Set α} :
                            s.InfiniteInfinite s

                            Alias of the reverse direction of Set.infinite_coe_iff.

                            theorem Set.Infinite.exists_not_mem_finite {α : Type u} {s : Set α} {t : Set α} (hs : s.Infinite) (ht : t.Finite) :
                            as, at
                            theorem Set.Infinite.exists_not_mem_finset {α : Type u} {s : Set α} (hs : s.Infinite) (t : Finset α) :
                            as, at
                            theorem Set.Finite.exists_not_mem {α : Type u} {s : Set α} [Infinite α] (hs : s.Finite) :
                            ∃ (a : α), as
                            theorem Finset.exists_not_mem {α : Type u} [Infinite α] (s : Finset α) :
                            ∃ (a : α), as
                            noncomputable def Set.Infinite.natEmbedding {α : Type u} (s : Set α) (h : s.Infinite) :
                            s

                            Embedding of into an infinite set.

                            Equations
                            Instances For
                              theorem Set.Infinite.exists_subset_card_eq {α : Type u} {s : Set α} (hs : s.Infinite) (n : ) :
                              ∃ (t : Finset α), t s t.card = n
                              theorem Set.infinite_of_finite_compl {α : Type u} [Infinite α] {s : Set α} (hs : s.Finite) :
                              s.Infinite
                              theorem Set.Finite.infinite_compl {α : Type u} [Infinite α] {s : Set α} (hs : s.Finite) :
                              s.Infinite
                              theorem Set.Infinite.diff {α : Type u} {s : Set α} {t : Set α} (hs : s.Infinite) (ht : t.Finite) :
                              (s \ t).Infinite
                              @[simp]
                              theorem Set.infinite_union {α : Type u} {s : Set α} {t : Set α} :
                              (s t).Infinite s.Infinite t.Infinite
                              theorem Set.Infinite.of_image {α : Type u} {β : Type v} (f : αβ) {s : Set α} (hs : (f '' s).Infinite) :
                              s.Infinite
                              theorem Set.infinite_image_iff {α : Type u} {β : Type v} {s : Set α} {f : αβ} (hi : Set.InjOn f s) :
                              (f '' s).Infinite s.Infinite
                              theorem Set.infinite_range_iff {α : Type u} {β : Type v} {f : αβ} (hi : Function.Injective f) :
                              (Set.range f).Infinite Infinite α
                              theorem Set.Infinite.image {α : Type u} {β : Type v} {s : Set α} {f : αβ} (hi : Set.InjOn f s) :
                              s.Infinite(f '' s).Infinite

                              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 : s.Infinite) (hb : b t) (hf : Set.InjOn (fun (a : α) => f a b) s) :
                              (Set.image2 f s t).Infinite
                              theorem Set.Infinite.image2_right {α : Type u} {β : Type v} {γ : Type x} {f : αβγ} {s : Set α} {t : Set β} {a : α} (ht : t.Infinite) (ha : a s) (hf : Set.InjOn (f a) t) :
                              (Set.image2 f s t).Infinite
                              theorem Set.infinite_image2 {α : Type u} {β : Type v} {γ : Type x} {f : αβγ} {s : Set α} {t : Set β} (hfs : bt, Set.InjOn (fun (a : α) => f a b) s) (hft : as, Set.InjOn (f a) t) :
                              (Set.image2 f s t).Infinite s.Infinite t.Nonempty t.Infinite s.Nonempty
                              theorem Set.finite_image2 {α : Type u} {β : Type v} {γ : Type x} {f : αβγ} {s : Set α} {t : Set β} (hfs : bt, Set.InjOn (fun (x : α) => f x b) s) (hft : as, Set.InjOn (f a) t) :
                              (Set.image2 f s t).Finite s.Finite t.Finite 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 : s.Infinite) :
                              t.Infinite
                              theorem Set.Infinite.exists_ne_map_eq_of_mapsTo {α : Type u} {β : Type v} {s : Set α} {t : Set β} {f : αβ} (hs : s.Infinite) (hf : Set.MapsTo f s t) (ht : t.Finite) :
                              xs, ys, x y f x = f y
                              theorem Set.infinite_range_of_injective {α : Type u} {β : Type v} [Infinite α] {f : αβ} (hi : Function.Injective f) :
                              (Set.range f).Infinite
                              theorem Set.infinite_of_injective_forall_mem {α : Type u} {β : Type v} [Infinite α] {s : Set β} {f : αβ} (hi : Function.Injective f) (hf : ∀ (x : α), f x s) :
                              s.Infinite
                              theorem Set.not_injOn_infinite_finite_image {α : Type u} {β : Type v} {f : αβ} {s : Set α} (h_inf : s.Infinite) (h_fin : (f '' s).Finite) :

                              Order properties #

                              theorem Set.infinite_of_forall_exists_gt {α : Type u} [Preorder α] [Nonempty α] {s : Set α} (h : ∀ (a : α), bs, a < b) :
                              s.Infinite
                              theorem Set.infinite_of_forall_exists_lt {α : Type u} [Preorder α] [Nonempty α] {s : Set α} (h : ∀ (a : α), bs, b < a) :
                              s.Infinite
                              theorem Set.finite_isTop (α : Type u_1) [PartialOrder α] :
                              {x : α | IsTop x}.Finite
                              theorem Set.finite_isBot (α : Type u_1) [PartialOrder α] :
                              {x : α | IsBot x}.Finite
                              theorem Set.Infinite.exists_lt_map_eq_of_mapsTo {α : Type u} {β : Type v} [LinearOrder α] {s : Set α} {t : Set β} {f : αβ} (hs : s.Infinite) (hf : Set.MapsTo f s t) (ht : t.Finite) :
                              xs, ys, x < y f x = f y
                              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 : t.Finite) :
                              ∃ (a : α) (b : α), a < b f a = f b
                              theorem Set.exists_min_image {α : Type u} {β : Type v} [LinearOrder β] (s : Set α) (f : αβ) (h1 : s.Finite) :
                              s.Nonemptyas, bs, f a f b
                              theorem Set.exists_max_image {α : Type u} {β : Type v} [LinearOrder β] (s : Set α) (f : αβ) (h1 : s.Finite) :
                              s.Nonemptyas, bs, f b f a
                              theorem Set.exists_lower_bound_image {α : Type u} {β : Type v} [Nonempty α] [LinearOrder β] (s : Set α) (f : αβ) (h : s.Finite) :
                              ∃ (a : α), bs, f a f b
                              theorem Set.exists_upper_bound_image {α : Type u} {β : Type v} [Nonempty α] [LinearOrder β] (s : Set α) (f : αβ) (h : s.Finite) :
                              ∃ (a : α), bs, 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 : s.Finite) {f : ιι'α} (hf : is, Monotone (f i)) :
                              ⨆ (j : ι'), is, f i j = is, ⨆ (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 : s.Finite) {f : ιι'α} (hf : is, Antitone (f i)) :
                              ⨆ (j : ι'), is, f i j = is, ⨆ (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 : s.Finite) {f : ιι'α} (hf : is, Monotone (f i)) :
                              ⨅ (j : ι'), is, f i j = is, ⨅ (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 : s.Finite) {f : ιι'α} (hf : is, Antitone (f i)) :
                              ⨅ (j : ι'), is, f i j = is, ⨅ (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 : I.Finite) (hs : iI, Monotone (s i)) :
                              (⋃ (j : ι'), I.pi fun (i : ι) => s i j) = I.pi fun (i : ι) => ⋃ (j : ι'), s i j
                              theorem Set.iUnion_univ_pi_of_monotone {ι : Type u_1} {ι' : Type u_2} [LinearOrder ι'] [Nonempty ι'] [Finite ι] {α : ιType u_3} {s : (i : ι) → ι'Set (α i)} (hs : ∀ (i : ι), Monotone (s i)) :
                              (⋃ (j : ι'), Set.univ.pi fun (i : ι) => s i j) = Set.univ.pi fun (i : ι) => ⋃ (j : ι'), s i j
                              theorem Set.finite_range_findGreatest {α : Type u} {P : αProp} [(x : α) → DecidablePred (P x)] {b : } :
                              (Set.range fun (x : α) => Nat.findGreatest (P x) b).Finite
                              theorem Set.Finite.exists_maximal_wrt {α : Type u} {β : Type v} [PartialOrder β] (f : αβ) (s : Set α) (h : s.Finite) (hs : s.Nonempty) :
                              as, a's, f a f a'f a = f a'
                              theorem Set.Finite.exists_maximal_wrt' {α : Type u} {β : Type v} [PartialOrder β] (f : αβ) (s : Set α) (h : (f '' s).Finite) (hs : s.Nonempty) :
                              as, a's, f a f a'f a = f a'

                              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 : s.Finite) (hs : s.Nonempty) :
                              as, a's, f a' f af a = f a'
                              theorem Set.Finite.exists_minimal_wrt' {α : Type u} {β : Type v} [PartialOrder β] (f : αβ) (s : Set α) (h : (f '' s).Finite) (hs : s.Nonempty) :
                              as, a's, f a' f af a = f a'

                              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 : s.Finite) :

                              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 : I.Finite) :
                              BddAbove (iI, S i) iI, 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} [Preorder α] [IsDirected α fun (x x_1 : α) => x x_1] [Nonempty α] {s : Set α} :
                              ¬BddAbove ss.Infinite
                              theorem Set.Finite.bddBelow {α : Type u} [Preorder α] [IsDirected α fun (x x_1 : α) => x x_1] [Nonempty α] {s : Set α} (hs : s.Finite) :

                              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 : I.Finite) :
                              BddBelow (iI, S i) iI, 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} [Preorder α] [IsDirected α fun (x x_1 : α) => x x_1] [Nonempty α] {s : Set α} :
                              ¬BddBelow ss.Infinite
                              theorem Finset.exists_card_eq {α : Type u} [Infinite α] (n : ) :
                              ∃ (s : Finset α), s.card = n
                              theorem Finset.bddAbove {α : Type u} [SemilatticeSup α] [Nonempty α] (s : Finset α) :

                              A finset is bounded above.

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

                              A finset is bounded below.

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

                              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 : xs, ys, zs, x < yy < zFalse) :
                              s.Finite

                              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 α) :
                              (s \ xs, ys, Set.Ioo x y).Finite
                              theorem Set.finite_diff_iUnion_Ioo' {α : Type u} [LinearOrder α] (s : Set α) :
                              (s \ ⋃ (x : s × s), Set.Ioo x.1 x.2).Finite
                              theorem Directed.exists_mem_subset_of_finset_subset_biUnion {α : Type u_1} {ι : Type u_2} [Nonempty ι] {f : ιSet α} (h : Directed (fun (x x_1 : Set α) => x x_1) f) {s : Finset α} (hs : s ⋃ (i : ι), f i) :
                              ∃ (i : ι), s f i
                              theorem DirectedOn.exists_mem_subset_of_finset_subset_biUnion {α : Type u_1} {ι : Type u_2} {f : ιSet α} {c : Set ι} (hn : c.Nonempty) (hc : DirectedOn (fun (i j : ι) => f i f j) c) {s : Finset α} (hs : s ic, f i) :
                              ic, s f i