def Function.graph' {α : Type u_1} {β : Type u_2} (f : α → β) : Set (α × β)

An alternate spelling of Function.graph, useful in proving inequalities of cardinals.

Equations

• Function.graph' f = {(x, y) : α × β | y = f x}

theorem Function.graph'_injective {α : Type u_1} {β : Type u_2} : Function.Injective Function.graph'

theorem Function.card_graph'_eq {α : Type (max u_1 u_2)} {β : Type u_1} (f : α → β) : Cardinal.mk ↑(Function.graph' f) = Cardinal.mk α

theorem Cardinal.mul_le_of_le {a b c : Cardinal.{u_1}} (hc : Cardinal.aleph0 ≤ c) (h1 : a ≤ c) (h2 : b ≤ c) : a * b ≤ c

theorem Cardinal.mk_biUnion_le_of_le_lift {α : Type u} {β : Type v} {s : Set α} {f : (x : α) → x ∈ s → Set β} (c : Cardinal.{v}) (h : ∀ (x : α) (h : x ∈ s), Cardinal.mk ↑(f x h) ≤ c) : Cardinal.lift.{u, v} (Cardinal.mk ↑(⋃ (x : α), ⋃ (h : x ∈ s), f x h)) ≤ Cardinal.lift.{v, u} (Cardinal.mk ↑s) * Cardinal.lift.{u, v} c

theorem Cardinal.mk_biUnion_le_of_le {α β : Type u_1} {s : Set α} {f : (x : α) → x ∈ s → Set β} (c : Cardinal.{u_1}) (h : ∀ (x : α) (h : x ∈ s), Cardinal.mk ↑(f x h) ≤ c) : Cardinal.mk ↑(⋃ (x : α), ⋃ (h : x ∈ s), f x h) ≤ Cardinal.mk ↑s * c

theorem Cardinal.mk_iUnion_le_of_le_lift {α : Type u} {β : Type v} {f : α → Set β} (c : Cardinal.{v}) (h : ∀ (x : α), Cardinal.mk ↑(f x) ≤ c) : Cardinal.lift.{u, v} (Cardinal.mk ↑(⋃ (x : α), f x)) ≤ Cardinal.lift.{v, u} (Cardinal.mk α) * Cardinal.lift.{u, v} c

theorem Cardinal.mk_iUnion_le_of_le {α β : Type u_1} {f : α → Set β} (c : Cardinal.{u_1}) (h : ∀ (x : α), Cardinal.mk ↑(f x) ≤ c) : Cardinal.mk ↑(⋃ (x : α), f x) ≤ Cardinal.mk α * c

theorem Cardinal.lift_isRegular (c : Cardinal.{u}) (h : c.IsRegular) : (Cardinal.lift.{v, u} c).IsRegular

theorem Cardinal.le_of_le_add {c d e : Cardinal.{u}} (h : c ≤ d + e) (hc : Cardinal.aleph0 ≤ c) (he : e < c) : c ≤ d

theorem Cardinal.mk_ne_zero_iff_nonempty {α : Type u_1} (s : Set α) : Cardinal.mk ↑s ≠ 0 ↔ s.Nonempty

theorem Cardinal.compl_nonempty_of_mk_lt {α : Type u_1} {s : Set α} (h : Cardinal.mk ↑s < Cardinal.mk α) : sᶜ.Nonempty

theorem Cardinal.mk_pow_le_of_mk_lt_ord_cof {α β : Type u_1} (hα : (Cardinal.mk α).IsStrongLimit) (hβ : Cardinal.mk β < (Cardinal.mk α).ord.cof) : Cardinal.mk α ^ Cardinal.mk β ≤ Cardinal.mk α

theorem Cardinal.pow_le_of_lt_ord_cof {c d : Cardinal.{u_1}} (hc : c.IsStrongLimit) (hd : d < c.ord.cof) : c ^ d ≤ c

If c is a strong limit and d is not "too large", then c ^ d = c. By "too large" here, we mean large enough to be a counterexample by König's theorem on cardinals: c < c ^ c.ord.cof.

theorem Cardinal.mk_fun_le (α : Type u_1) (β : Type u_2) : Cardinal.mk (α → β) ≤ Cardinal.mk (Set (α × β))

theorem Cardinal.mk_power_le_two_power (α β : Type u_1) : Cardinal.mk α ^ Cardinal.mk β ≤ Cardinal.aleph0 ⊔ (2 ^ Cardinal.mk α ⊔ 2 ^ Cardinal.mk β)

theorem Cardinal.power_le_two_power (c d : Cardinal.{u_1}) : c ^ d ≤ Cardinal.aleph0 ⊔ (2 ^ c ⊔ 2 ^ d)

theorem Cardinal.pow_lt_of_lt {c d e : Cardinal.{u_1}} (hc : c.IsStrongLimit) (hd : d < c) (he : e < c) : d ^ e < c

Strong limit cardinals are closed under exponentials.

theorem Cardinal.card_codom_le_of_functional {α β : Type u_1} {r : Rel α β} (hr : r.Functional) : Cardinal.mk ↑r.codom ≤ Cardinal.mk ↑r.dom

theorem Cardinal.card_codom_le_of_coinjective {α β : Type u_1} {r : Rel α β} (hr : r.Coinjective) : Cardinal.mk ↑r.codom ≤ Cardinal.mk ↑r.dom