Documentation

Mathlib.SetTheory.Cardinal.Basic

Cardinal Numbers #

We define cardinal numbers as a quotient of types under the equivalence relation of equinumerity.

Main definitions #

Main instances #

Main Statements #

Implementation notes #

References #

Tags #

cardinal number, cardinal arithmetic, cardinal exponentiation, aleph, Cantor's theorem, König's theorem, Konig's theorem

Definition of cardinals #

The equivalence relation on types given by equivalence (bijective correspondence) of types. Quotienting by this equivalence relation gives the cardinal numbers.

Equations
def Cardinal :
Type (u + 1)

Cardinal.{u} is the type of cardinal numbers in Type u, defined as the quotient of Type u by existence of an equivalence (a bijection with explicit inverse).

Equations
Instances For

    The cardinal number of a type

    Equations
    Instances For

      The cardinal number of a type

      Equations
      Instances For
        theorem Cardinal.inductionOn {p : Cardinal.{u_1}Prop} (c : Cardinal.{u_1}) (h : ∀ (α : Type u_1), p (Cardinal.mk α)) :
        p c
        theorem Cardinal.inductionOn₂ {p : Cardinal.{u_1}Cardinal.{u_2}Prop} (c₁ : Cardinal.{u_1}) (c₂ : Cardinal.{u_2}) (h : ∀ (α : Type u_1) (β : Type u_2), p (Cardinal.mk α) (Cardinal.mk β)) :
        p c₁ c₂
        theorem Cardinal.inductionOn₃ {p : Cardinal.{u_1}Cardinal.{u_2}Cardinal.{u_3}Prop} (c₁ : Cardinal.{u_1}) (c₂ : Cardinal.{u_2}) (c₃ : Cardinal.{u_3}) (h : ∀ (α : Type u_1) (β : Type u_2) (γ : Type u_3), p (Cardinal.mk α) (Cardinal.mk β) (Cardinal.mk γ)) :
        p c₁ c₂ c₃
        theorem Cardinal.induction_on_pi {ι : Type u} {p : (ιCardinal.{v})Prop} (f : ιCardinal.{v}) (h : ∀ (f : ιType v), p fun (i : ι) => Cardinal.mk (f i)) :
        p f
        theorem Cardinal.eq {α : Type u} {β : Type u} :
        @[simp]
        theorem Cardinal.mk'_def (α : Type u) :
        α = Cardinal.mk α

        The representative of the cardinal of a type is equivalent to the original type.

        Equations
        • Cardinal.outMkEquiv = .some
        Instances For
          theorem Cardinal.mk_congr {α : Type u} {β : Type u} (e : α β) :
          theorem Equiv.cardinal_eq {α : Type u} {β : Type u} (e : α β) :

          Alias of Cardinal.mk_congr.

          def Cardinal.map (f : Type u → Type v) (hf : (α β : Type u) → α βf α f β) :

          Lift a function between Type*s to a function between Cardinals.

          Equations
          Instances For
            @[simp]
            theorem Cardinal.map_mk (f : Type u → Type v) (hf : (α β : Type u) → α βf α f β) (α : Type u) :
            def Cardinal.map₂ (f : Type u → Type v → Type w) (hf : (α β : Type u) → (γ δ : Type v) → α βγ δf α γ f β δ) :

            Lift a binary operation Type* → Type* → Type* to a binary operation on Cardinals.

            Equations
            Instances For

              We define the order on cardinal numbers by #α ≤ #β if and only if there exists an embedding (injective function) from α to β.

              Equations
              Equations
              • One or more equations did not get rendered due to their size.
              theorem Cardinal.le_def (α : Type u) (β : Type u) :
              theorem Cardinal.mk_le_of_injective {α : Type u} {β : Type u} {f : αβ} (hf : Function.Injective f) :
              theorem Function.Embedding.cardinal_le {α : Type u} {β : Type u} (f : α β) :
              theorem Cardinal.mk_le_of_surjective {α : Type u} {β : Type u} {f : αβ} (hf : Function.Surjective f) :
              theorem Cardinal.le_mk_iff_exists_set {c : Cardinal.{u}} {α : Type u} :
              c Cardinal.mk α ∃ (p : Set α), Cardinal.mk p = c
              theorem Cardinal.mk_set_le {α : Type u} (s : Set α) :

              Lifting cardinals to a higher universe #

              The universe lift operation on cardinals. You can specify the universes explicitly with lift.{u v} : Cardinal.{v} → Cardinal.{max v u}

              Equations
              Instances For
                @[simp]

                lift.{max u v, u} equals lift.{v, u}.

                @[simp]

                lift.{max v u, u} equals lift.{v, u}.

                @[simp]

                A cardinal lifted to a lower or equal universe equals itself.

                @[simp]

                A cardinal lifted to the same universe equals itself.

                A cardinal lifted to the zero universe equals itself.

                @[simp]
                theorem Cardinal.mk_preimage_down {α : Type u} {s : Set α} :

                A variant of Cardinal.lift_mk_le with specialized universes. Because Lean often can not realize it should use this specialization itself, we provide this statement separately so you don't have to solve the specialization problem either.

                A variant of Cardinal.lift_mk_eq with specialized universes. Because Lean often can not realize it should use this specialization itself, we provide this statement separately so you don't have to solve the specialization problem either.

                Basic cardinals #

                @[simp]
                theorem Cardinal.mk_eq_zero (α : Type u) [IsEmpty α] :
                @[simp]
                theorem Cardinal.mk_ne_zero (α : Type u) [Nonempty α] :
                theorem Cardinal.mk_eq_one (α : Type u) [Unique α] :
                @[simp]
                theorem Cardinal.mk_le_one_iff_set_subsingleton {α : Type u} {s : Set α} :
                Cardinal.mk s 1 s.Subsingleton
                theorem Set.Subsingleton.cardinal_mk_le_one {α : Type u} {s : Set α} :
                s.SubsingletonCardinal.mk s 1

                Alias of the reverse direction of Cardinal.mk_le_one_iff_set_subsingleton.

                Equations
                theorem Cardinal.add_def (α : Type u) (β : Type u) :
                @[simp]
                @[simp]
                theorem Cardinal.mk_fintype (α : Type u) [h : Fintype α] :
                Equations
                theorem Cardinal.mul_def (α : Type u) (β : Type u) :

                The cardinal exponential. #α ^ #β is the cardinal of β → α.

                Equations
                theorem Cardinal.power_def (α : Type u) (β : Type u) :
                @[simp]
                theorem Cardinal.power_zero (a : Cardinal.{u_1}) :
                a ^ 0 = 1
                @[simp]
                theorem Cardinal.power_one (a : Cardinal.{u}) :
                a ^ 1 = a
                theorem Cardinal.power_add (a : Cardinal.{u_1}) (b : Cardinal.{u_1}) (c : Cardinal.{u_1}) :
                a ^ (b + c) = a ^ b * a ^ c
                @[simp]
                theorem Cardinal.one_power {a : Cardinal.{u_1}} :
                1 ^ a = 1
                @[simp]
                theorem Cardinal.zero_power {a : Cardinal.{u_1}} :
                a 00 ^ a = 0
                theorem Cardinal.mul_power {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} {c : Cardinal.{u_1}} :
                (a * b) ^ c = a ^ c * b ^ c
                theorem Cardinal.power_mul {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} {c : Cardinal.{u_1}} :
                a ^ (b * c) = (a ^ b) ^ c
                @[simp]
                theorem Cardinal.pow_cast_right (a : Cardinal.{u}) (n : ) :
                a ^ n = a ^ n
                @[simp]
                theorem Cardinal.mk_set {α : Type u} :
                @[simp]
                theorem Cardinal.mk_powerset {α : Type u} (s : Set α) :

                A variant of Cardinal.mk_set expressed in terms of a Set instead of a Type.

                Order properties #

                Equations
                • One or more equations did not get rendered due to their size.
                Equations
                • One or more equations did not get rendered due to their size.
                theorem Cardinal.power_le_power_left {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} {c : Cardinal.{u_1}} :
                a 0b ca ^ b a ^ c
                theorem Cardinal.self_le_power (a : Cardinal.{u_1}) {b : Cardinal.{u_1}} (hb : 1 b) :
                a a ^ b
                theorem Cardinal.cantor (a : Cardinal.{u}) :
                a < 2 ^ a

                Cantor's theorem

                theorem Cardinal.power_pos {a : Cardinal.{u_1}} (b : Cardinal.{u_1}) (ha : 0 < a) :
                0 < a ^ b
                theorem Cardinal.lt_wf :
                WellFounded fun (x1 x2 : Cardinal.{u}) => x1 < x2
                instance Cardinal.wo :
                IsWellOrder Cardinal.{u} fun (x1 x2 : Cardinal.{u}) => x1 < x2
                Equations
                @[simp]
                theorem Cardinal.sInf_eq_zero_iff {s : Set Cardinal.{u_1}} :
                sInf s = 0 s = as, a = 0
                theorem Cardinal.iInf_eq_zero_iff {ι : Sort u_1} {f : ιCardinal.{u_2}} :
                ⨅ (i : ι), f i = 0 IsEmpty ι ∃ (i : ι), f i = 0
                theorem Cardinal.iSup_of_empty {ι : Sort u_1} (f : ιCardinal.{u_2}) [IsEmpty ι] :
                iSup f = 0

                A variant of ciSup_of_empty but with 0 on the RHS for convenience

                @[simp]
                theorem Cardinal.lift_iInf {ι : Sort u_1} (f : ιCardinal.{v}) :

                Note that the successor of c is not the same as c + 1 except in the case of finite c.

                Equations
                @[deprecated Order.IsSuccLimit]

                A cardinal is a limit if it is not zero or a successor cardinal. Note that ℵ₀ is a limit cardinal by this definition, but 0 isn't. Deprecated. Use Order.IsSuccLimit instead.

                Equations
                Instances For
                  @[deprecated Order.IsSuccLimit.isSuccPrelimit]
                  @[deprecated Cardinal.ne_zero_of_isSuccLimit]
                  theorem Cardinal.IsLimit.ne_zero {c : Cardinal.{u_1}} (h : c.IsLimit) :
                  c 0
                  @[deprecated Cardinal.IsLimit.isSuccPrelimit]

                  Alias of Cardinal.IsLimit.isSuccPrelimit.

                  @[deprecated Order.IsSuccLimit.succ_lt]
                  theorem Cardinal.IsLimit.succ_lt {x : Cardinal.{u_1}} {c : Cardinal.{u_1}} (h : c.IsLimit) :
                  x < cOrder.succ x < c
                  @[deprecated Cardinal.isSuccPrelimit_zero]

                  Alias of Cardinal.isSuccPrelimit_zero.

                  Indexed cardinal sum #

                  The indexed sum of cardinals is the cardinality of the indexed disjoint union, i.e. sigma type.

                  Equations
                  Instances For
                    theorem Cardinal.le_sum {ι : Type u_1} (f : ιCardinal.{max u_1 u_2} ) (i : ι) :
                    @[simp]
                    theorem Cardinal.mk_sigma {ι : Type u_2} (f : ιType u_1) :
                    Cardinal.mk ((i : ι) × f i) = Cardinal.sum fun (i : ι) => Cardinal.mk (f i)
                    theorem Cardinal.mk_sigma_arrow {ι : Type u_3} (α : Type u_1) (f : ιType u_2) :
                    Cardinal.mk (Sigma fα) = Cardinal.mk ((i : ι) → f iα)
                    theorem Cardinal.sum_const' (ι : Type u) (a : Cardinal.{u}) :
                    (Cardinal.sum fun (x : ι) => a) = Cardinal.mk ι * a
                    @[simp]
                    theorem Cardinal.sum_add_distrib {ι : Type u_1} (f : ιCardinal.{u_2}) (g : ιCardinal.{u_2}) :
                    @[simp]
                    theorem Cardinal.sum_add_distrib' {ι : Type u_1} (f : ιCardinal.{u_2}) (g : ιCardinal.{u_2}) :
                    (Cardinal.sum fun (i : ι) => f i + g i) = Cardinal.sum f + Cardinal.sum g
                    theorem Cardinal.sum_le_sum {ι : Type u_1} (f : ιCardinal.{u_2}) (g : ιCardinal.{u_2}) (H : ∀ (i : ι), f i g i) :
                    theorem Cardinal.mk_le_mk_mul_of_mk_preimage_le {α : Type u} {β : Type u} {c : Cardinal.{u}} (f : αβ) (hf : ∀ (b : β), Cardinal.mk (f ⁻¹' {b}) c) :

                    Well-ordering theorem #

                    An embedding of any type to the set of cardinals in its universe.

                    Equations
                    Instances For
                      def WellOrderingRel {α : Type u} :
                      ααProp

                      Any type can be endowed with a well order, obtained by pulling back the well order over cardinals by some embedding.

                      Equations
                      Instances For
                        instance WellOrderingRel.isWellOrder {α : Type u} :
                        IsWellOrder α WellOrderingRel
                        Equations
                        • =
                        instance IsWellOrder.subtype_nonempty {α : Type u} :
                        Nonempty { r : ααProp // IsWellOrder α r }
                        Equations
                        • =

                        Small sets of cardinals #

                        The range of an indexed cardinal function, whose outputs live in a higher universe than the inputs, is always bounded above.

                        Equations
                        • =
                        Equations
                        • =
                        Equations
                        • =
                        Equations
                        • =
                        Equations
                        • =
                        Equations
                        • =

                        A set of cardinals is bounded above iff it's small, i.e. it corresponds to a usual ZFC set.

                        Bounds on suprema #

                        The lift of a supremum is the supremum of the lifts.

                        theorem Cardinal.lift_iSup {ι : Type v} {f : ιCardinal.{w}} (hf : BddAbove (Set.range f)) :

                        The lift of a supremum is the supremum of the lifts.

                        theorem Cardinal.lift_iSup_le {ι : Type v} {f : ιCardinal.{w}} {t : Cardinal.{max u w} } (hf : BddAbove (Set.range f)) (w : ∀ (i : ι), Cardinal.lift.{u, w} (f i) t) :

                        To prove that the lift of a supremum is bounded by some cardinal t, it suffices to show that the lift of each cardinal is bounded by t.

                        @[simp]
                        theorem Cardinal.lift_iSup_le_iff {ι : Type v} {f : ιCardinal.{w}} (hf : BddAbove (Set.range f)) {t : Cardinal.{max u w} } :
                        theorem Cardinal.lift_iSup_le_lift_iSup {ι : Type v} {ι' : Type v'} {f : ιCardinal.{w}} {f' : ι'Cardinal.{w'}} (hf : BddAbove (Set.range f)) (hf' : BddAbove (Set.range f')) {g : ιι'} (h : ∀ (i : ι), Cardinal.lift.{w', w} (f i) Cardinal.lift.{w, w'} (f' (g i))) :

                        To prove an inequality between the lifts to a common universe of two different supremums, it suffices to show that the lift of each cardinal from the smaller supremum if bounded by the lift of some cardinal from the larger supremum.

                        theorem Cardinal.lift_iSup_le_lift_iSup' {ι : Type v} {ι' : Type v'} {f : ιCardinal.{v}} {f' : ι'Cardinal.{v'}} (hf : BddAbove (Set.range f)) (hf' : BddAbove (Set.range f')) (g : ιι') (h : ∀ (i : ι), Cardinal.lift.{v', v} (f i) Cardinal.lift.{v, v'} (f' (g i))) :

                        A variant of lift_iSup_le_lift_iSup with universes specialized via w = v and w' = v'. This is sometimes necessary to avoid universe unification issues.

                        theorem Cardinal.exists_eq_of_iSup_eq_of_not_isSuccPrelimit {ι : Type u} (f : ιCardinal.{v}) (ω : Cardinal.{v}) (hω : ¬Order.IsSuccPrelimit ω) (h : ⨆ (i : ι), f i = ω) :
                        ∃ (i : ι), f i = ω
                        theorem Cardinal.exists_eq_of_iSup_eq_of_not_isSuccLimit {ι : Type u} [hι : Nonempty ι] (f : ιCardinal.{v}) (hf : BddAbove (Set.range f)) {c : Cardinal.{v}} (hc : ¬Order.IsSuccLimit c) (h : ⨆ (i : ι), f i = c) :
                        ∃ (i : ι), f i = c
                        @[deprecated Cardinal.exists_eq_of_iSup_eq_of_not_isSuccLimit]
                        theorem Cardinal.exists_eq_of_iSup_eq_of_not_isLimit {ι : Type u} [hι : Nonempty ι] (f : ιCardinal.{v}) (hf : BddAbove (Set.range f)) (ω : Cardinal.{v}) (hω : ¬ω.IsLimit) (h : ⨆ (i : ι), f i = ω) :
                        ∃ (i : ι), f i = ω

                        Indexed cardinal prod #

                        The indexed product of cardinals is the cardinality of the Pi type (dependent product).

                        Equations
                        Instances For
                          @[simp]
                          theorem Cardinal.mk_pi {ι : Type u} (α : ιType v) :
                          Cardinal.mk ((i : ι) → α i) = Cardinal.prod fun (i : ι) => Cardinal.mk (α i)
                          theorem Cardinal.prod_const' (ι : Type u) (a : Cardinal.{u}) :
                          (Cardinal.prod fun (x : ι) => a) = a ^ Cardinal.mk ι
                          theorem Cardinal.prod_le_prod {ι : Type u_1} (f : ιCardinal.{u_2}) (g : ιCardinal.{u_2}) (H : ∀ (i : ι), f i g i) :
                          @[simp]
                          theorem Cardinal.prod_eq_zero {ι : Type u_1} (f : ιCardinal.{u}) :
                          Cardinal.prod f = 0 ∃ (i : ι), f i = 0
                          theorem Cardinal.prod_ne_zero {ι : Type u_1} (f : ιCardinal.{u_2}) :
                          Cardinal.prod f 0 ∀ (i : ι), f i 0
                          theorem Cardinal.power_sum {ι : Type u_1} (a : Cardinal.{max u_1 u_2} ) (f : ιCardinal.{max u_1 u_2} ) :
                          a ^ Cardinal.sum f = Cardinal.prod fun (i : ι) => a ^ f i
                          theorem Cardinal.prod_eq_of_fintype {α : Type u} [h : Fintype α] (f : αCardinal.{v}) :
                          theorem Cardinal.sum_lt_prod {ι : Type u_1} (f : ιCardinal.{u_2}) (g : ιCardinal.{u_2}) (H : ∀ (i : ι), f i < g i) :

                          König's theorem

                          The first infinite cardinal aleph0 #

                          ℵ₀ is the smallest infinite cardinal.

                          Equations
                          Instances For

                            ℵ₀ is the smallest infinite cardinal.

                            Equations
                            Instances For

                              Properties about the cast from #

                              theorem Cardinal.mk_fin (n : ) :
                              Cardinal.mk (Fin n) = n
                              @[simp]
                              @[simp]
                              @[simp]
                              @[simp]
                              @[simp]
                              @[simp]
                              theorem Cardinal.mk_coe_finset {α : Type u} {s : Finset α} :
                              Cardinal.mk { x : α // x s } = s.card
                              theorem Cardinal.card_le_of_finset {α : Type u_1} (s : Finset α) :
                              s.card Cardinal.mk α
                              theorem Cardinal.natCast_pow {m : } {n : } :
                              (m ^ n) = m ^ n
                              theorem Cardinal.natCast_le {m : } {n : } :
                              m n m n
                              theorem Cardinal.natCast_lt {m : } {n : } :
                              m < n m < n
                              theorem Cardinal.natCast_inj {m : } {n : } :
                              m = n m = n
                              theorem Cardinal.nat_succ (n : ) :
                              n.succ = Order.succ n
                              theorem Cardinal.succ_natCast (n : ) :
                              Order.succ n = n + 1
                              theorem Cardinal.natCast_add_one_le_iff {n : } {c : Cardinal.{u_1}} :
                              n + 1 c n < c
                              theorem Cardinal.exists_finset_le_card (α : Type u_1) (n : ) (h : n Cardinal.mk α) :
                              ∃ (s : Finset α), n s.card
                              theorem Cardinal.card_le_of {α : Type u} {n : } (H : ∀ (s : Finset α), s.card n) :
                              theorem Cardinal.cantor' (a : Cardinal.{u_1}) {b : Cardinal.{u_1}} (hb : 1 < b) :
                              a < b ^ a
                              @[simp]

                              Properties about aleph0 #

                              theorem Cardinal.lt_aleph0 {c : Cardinal.{u_1}} :
                              c < Cardinal.aleph0 ∃ (n : ), c = n
                              @[deprecated Cardinal.isSuccLimit_aleph0]
                              @[deprecated Cardinal.not_isSuccLimit_natCast]
                              theorem Cardinal.not_isLimit_natCast (n : ) :
                              ¬(↑n).IsLimit
                              @[deprecated Cardinal.aleph0_le_of_isSuccLimit]
                              theorem Cardinal.exists_eq_natCast_of_iSup_eq {ι : Type u} [Nonempty ι] (f : ιCardinal.{v}) (hf : BddAbove (Set.range f)) (n : ) (h : ⨆ (i : ι), f i = n) :
                              ∃ (i : ι), f i = n
                              theorem Cardinal.mk_eq_nat_iff {α : Type u} {n : } :
                              Cardinal.mk α = n Nonempty (α Fin n)
                              theorem Set.Finite.lt_aleph0 {α : Type u} {S : Set α} :
                              S.FiniteCardinal.mk S < Cardinal.aleph0

                              Alias of the reverse direction of Cardinal.lt_aleph0_iff_set_finite.

                              @[simp]
                              theorem Cardinal.lt_aleph0_iff_subtype_finite {α : Type u} {p : αProp} :
                              Cardinal.mk { x : α // p x } < Cardinal.aleph0 {x : α | p x}.Finite
                              theorem Set.Countable.le_aleph0 {α : Type u} {s : Set α} :
                              s.CountableCardinal.mk s Cardinal.aleph0

                              Alias of the reverse direction of Cardinal.le_aleph0_iff_set_countable.

                              @[simp]
                              theorem Cardinal.le_aleph0_iff_subtype_countable {α : Type u} {p : αProp} :
                              Cardinal.mk { x : α // p x } Cardinal.aleph0 {x : α | p x}.Countable
                              theorem Set.countable_infinite_iff_nonempty_denumerable {α : Type u_1} {s : Set α} :
                              s.Countable s.Infinite Nonempty (Denumerable s)
                              @[simp]
                              @[simp]
                              theorem Cardinal.exists_nat_eq_of_le_nat {c : Cardinal.{u_1}} {n : } (h : c n) :
                              mn, c = m

                              Cardinalities of basic sets and types #

                              theorem Cardinal.mk_singleton {α : Type u} (x : α) :
                              Cardinal.mk {x} = 1
                              @[simp]
                              theorem Cardinal.mk_vector (α : Type u) (n : ) :
                              theorem Cardinal.mk_quot_le {α : Type u} {r : ααProp} :
                              theorem Cardinal.mk_subtype_le_of_subset {α : Type u} {p : αProp} {q : αProp} (h : ∀ ⦃x : α⦄, p xq x) :
                              theorem Cardinal.mk_emptyCollection_iff {α : Type u} {s : Set α} :
                              Cardinal.mk s = 0 s =
                              @[simp]
                              theorem Cardinal.mk_univ {α : Type u} :
                              Cardinal.mk Set.univ = Cardinal.mk α
                              theorem Cardinal.mk_image_le {α : Type u} {β : Type u} {f : αβ} {s : Set α} :
                              theorem Cardinal.mk_image_le_lift {α : Type u} {β : Type v} {f : αβ} {s : Set α} :
                              theorem Cardinal.mk_range_le {α : Type u} {β : Type u} {f : αβ} :
                              theorem Cardinal.mk_range_eq {α : Type u} {β : Type u} (f : αβ) (h : Function.Injective f) :
                              theorem Cardinal.mk_image_eq_of_injOn {α : Type u} {β : Type u} (f : αβ) (s : Set α) (h : Set.InjOn f s) :
                              Cardinal.mk (f '' s) = Cardinal.mk s
                              theorem Cardinal.mk_image_eq_of_injOn_lift {α : Type u} {β : Type v} (f : αβ) (s : Set α) (h : Set.InjOn f s) :
                              theorem Cardinal.mk_image_eq {α : Type u} {β : Type u} {f : αβ} {s : Set α} (hf : Function.Injective f) :
                              Cardinal.mk (f '' s) = Cardinal.mk s
                              theorem Cardinal.mk_image_eq_lift {α : Type u} {β : Type v} (f : αβ) (s : Set α) (h : Function.Injective f) :
                              theorem Cardinal.mk_iUnion_le_sum_mk {α : Type u} {ι : Type u} {f : ιSet α} :
                              Cardinal.mk (⋃ (i : ι), f i) Cardinal.sum fun (i : ι) => Cardinal.mk (f i)
                              theorem Cardinal.mk_iUnion_le_sum_mk_lift {α : Type u} {ι : Type v} {f : ιSet α} :
                              Cardinal.lift.{v, u} (Cardinal.mk (⋃ (i : ι), f i)) Cardinal.sum fun (i : ι) => Cardinal.mk (f i)
                              theorem Cardinal.mk_iUnion_eq_sum_mk {α : Type u} {ι : Type u} {f : ιSet α} (h : Pairwise fun (i j : ι) => Disjoint (f i) (f j)) :
                              Cardinal.mk (⋃ (i : ι), f i) = Cardinal.sum fun (i : ι) => Cardinal.mk (f i)
                              theorem Cardinal.mk_iUnion_eq_sum_mk_lift {α : Type u} {ι : Type v} {f : ιSet α} (h : Pairwise fun (i j : ι) => Disjoint (f i) (f j)) :
                              Cardinal.lift.{v, u} (Cardinal.mk (⋃ (i : ι), f i)) = Cardinal.sum fun (i : ι) => Cardinal.mk (f i)
                              theorem Cardinal.mk_iUnion_le {α : Type u} {ι : Type u} (f : ιSet α) :
                              Cardinal.mk (⋃ (i : ι), f i) Cardinal.mk ι * ⨆ (i : ι), Cardinal.mk (f i)
                              theorem Cardinal.mk_iUnion_le_lift {α : Type u} {ι : Type v} (f : ιSet α) :
                              theorem Cardinal.mk_sUnion_le {α : Type u} (A : Set (Set α)) :
                              Cardinal.mk (⋃₀ A) Cardinal.mk A * ⨆ (s : A), Cardinal.mk s
                              theorem Cardinal.mk_biUnion_le {ι : Type u} {α : Type u} (A : ιSet α) (s : Set ι) :
                              Cardinal.mk (⋃ xs, A x) Cardinal.mk s * ⨆ (x : s), Cardinal.mk (A x)
                              theorem Cardinal.mk_biUnion_le_lift {α : Type u} {ι : Type v} (A : ιSet α) (s : Set ι) :
                              Cardinal.lift.{v, u} (Cardinal.mk (⋃ xs, A x)) Cardinal.lift.{u, v} (Cardinal.mk s) * ⨆ (x : s), Cardinal.lift.{v, u} (Cardinal.mk (A x))
                              theorem Cardinal.mk_set_eq_nat_iff_finset {α : Type u_1} {s : Set α} {n : } :
                              Cardinal.mk s = n ∃ (t : Finset α), t = s t.card = n
                              theorem Cardinal.mk_eq_nat_iff_finset {α : Type u} {n : } :
                              Cardinal.mk α = n ∃ (t : Finset α), t = Set.univ t.card = n
                              theorem Cardinal.mk_eq_nat_iff_fintype {α : Type u} {n : } :
                              Cardinal.mk α = n ∃ (h : Fintype α), Fintype.card α = n
                              theorem Cardinal.mk_union_add_mk_inter {α : Type u} {S : Set α} {T : Set α} :
                              Cardinal.mk (S T) + Cardinal.mk (S T) = Cardinal.mk S + Cardinal.mk T
                              theorem Cardinal.mk_union_le {α : Type u} (S : Set α) (T : Set α) :

                              The cardinality of a union is at most the sum of the cardinalities of the two sets.

                              theorem Cardinal.mk_union_of_disjoint {α : Type u} {S : Set α} {T : Set α} (H : Disjoint S T) :
                              theorem Cardinal.mk_insert {α : Type u} {s : Set α} {a : α} (h : as) :
                              Cardinal.mk (insert a s) = Cardinal.mk s + 1
                              theorem Cardinal.mk_insert_le {α : Type u} {s : Set α} {a : α} :
                              theorem Cardinal.mk_sum_compl {α : Type u_1} (s : Set α) :
                              theorem Cardinal.mk_le_mk_of_subset {α : Type u_1} {s : Set α} {t : Set α} (h : s t) :
                              theorem Cardinal.mk_le_iff_forall_finset_subset_card_le {α : Type u} {n : } {t : Set α} :
                              Cardinal.mk t n ∀ (s : Finset α), s ts.card n
                              theorem Cardinal.mk_subtype_mono {α : Type u} {p : αProp} {q : αProp} (h : ∀ (x : α), p xq x) :
                              Cardinal.mk { x : α // p x } Cardinal.mk { x : α // q x }
                              theorem Cardinal.le_mk_diff_add_mk {α : Type u} (S : Set α) (T : Set α) :
                              theorem Cardinal.mk_diff_add_mk {α : Type u} {S : Set α} {T : Set α} (h : T S) :
                              Cardinal.mk (S \ T) + Cardinal.mk T = Cardinal.mk S
                              theorem Cardinal.mk_subtype_of_equiv {α : Type u} {β : Type u} (p : βProp) (e : α β) :
                              Cardinal.mk { a : α // p (e a) } = Cardinal.mk { b : β // p b }
                              theorem Cardinal.mk_sep {α : Type u} (s : Set α) (t : αProp) :
                              Cardinal.mk {x : α | x s t x} = Cardinal.mk {x : s | t x}
                              theorem Cardinal.mk_preimage_of_injective_of_subset_range {α : Type u} {β : Type u} (f : αβ) (s : Set β) (h : Function.Injective f) (h2 : s Set.range f) :
                              theorem Cardinal.mk_preimage_of_injective {α : Type u} {β : Type u} (f : αβ) (s : Set β) (h : Function.Injective f) :
                              theorem Cardinal.mk_preimage_of_subset_range {α : Type u} {β : Type u} (f : αβ) (s : Set β) (h : s Set.range f) :
                              theorem Cardinal.mk_subset_ge_of_subset_image_lift {α : Type u} {β : Type v} (f : αβ) {s : Set α} {t : Set β} (h : t f '' s) :
                              theorem Cardinal.mk_subset_ge_of_subset_image {α : Type u} {β : Type u} (f : αβ) {s : Set α} {t : Set β} (h : t f '' s) :
                              Cardinal.mk t Cardinal.mk {x : α | x s f x t}
                              theorem Cardinal.le_mk_iff_exists_subset {c : Cardinal.{u}} {α : Type u} {s : Set α} :
                              c Cardinal.mk s ps, Cardinal.mk p = c
                              theorem Cardinal.two_le_iff {α : Type u} :
                              2 Cardinal.mk α ∃ (x : α) (y : α), x y
                              theorem Cardinal.two_le_iff' {α : Type u} (x : α) :
                              2 Cardinal.mk α ∃ (y : α), y x
                              theorem Cardinal.mk_eq_two_iff {α : Type u} :
                              Cardinal.mk α = 2 ∃ (x : α) (y : α), x y {x, y} = Set.univ
                              theorem Cardinal.mk_eq_two_iff' {α : Type u} (x : α) :
                              Cardinal.mk α = 2 ∃! y : α, y x
                              theorem Cardinal.exists_not_mem_of_length_lt {α : Type u_1} (l : List α) (h : l.length < Cardinal.mk α) :
                              ∃ (z : α), zl
                              theorem Cardinal.three_le {α : Type u_1} (h : 3 Cardinal.mk α) (x : α) (y : α) :
                              ∃ (z : α), z x z y

                              powerlt operation #

                              The function a ^< b, defined as the supremum of a ^ c for c < b.

                              Equations
                              Instances For

                                The function a ^< b, defined as the supremum of a ^ c for c < b.

                                Equations
                                Instances For
                                  theorem Cardinal.le_powerlt {b : Cardinal.{u}} {c : Cardinal.{u}} (a : Cardinal.{u}) (h : c < b) :
                                  a ^ c a ^< b
                                  theorem Cardinal.powerlt_le {a : Cardinal.{u}} {b : Cardinal.{u}} {c : Cardinal.{u}} :
                                  a ^< b c x < b, a ^ x c
                                  theorem Cardinal.powerlt_min {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} {c : Cardinal.{u_1}} :
                                  a ^< min b c = min (a ^< b) (a ^< c)
                                  theorem Cardinal.powerlt_max {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} {c : Cardinal.{u_1}} :
                                  a ^< max b c = max (a ^< b) (a ^< c)
                                  theorem Cardinal.zero_powerlt {a : Cardinal.{u_1}} (h : a 0) :
                                  0 ^< a = 1
                                  @[simp]