theorem nonempty_equiv_comm {α : Type u_1} {β : Type u_2} : Nonempty (α ≃ β) ↔ Nonempty (β ≃ α)

@[simp]

theorem nonempty_equiv_refl {α : Type u_1} : Nonempty (α ≃ α)

theorem nonempty_equiv_set_empty_empty {α : Type u_1} {β : Type u_2} : Nonempty (↑∅ ≃ ↑∅)

@[simp]

theorem nonempty_equiv_set_empty_iff {α : Type u_1} {β : Type u_2} {s : Set α} : Nonempty (↑s ≃ ↑∅) ↔ s = ∅

theorem nonempty_equiv_trans {α : Type u_1} {γ : Type u_2} (β : Type u_3) (h₁ : Nonempty (α ≃ β)) (h₂ : Nonempty (β ≃ γ)) : Nonempty (α ≃ γ)

theorem nonempty_equiv_set_univ_self {α : Type u_1} : Nonempty (α ≃ ↑Set.univ)

theorem nonempty_equiv_set_univ_self' {α : Type u_1} : Nonempty (↑Set.univ ≃ α)

theorem nonempty_equiv_set_univ_set_univ_iff {α β : Type u} : Nonempty (↑Set.univ ≃ ↑Set.univ) ↔ Nonempty (α ≃ β)

@[simp]

theorem nonempty_equiv_set_univ_iff {α β : Type u} : Nonempty (α ≃ ↑Set.univ) ↔ Nonempty (α ≃ β)

@[simp]

theorem nonempty_equiv_set_univ_iff' {α β : Type u} : Nonempty (↑Set.univ ≃ β) ↔ Nonempty (α ≃ β)

theorem Cardinal.mk_eq_of_fintype_card {α : Type u_1} [h : Fintype α] {n : ℕ} (h₁ : Fintype.card α = n) : mk α = ↑n

@[simp]

theorem Cardinal.mk_subtype_const_true {α : Type u_1} : mk { _x : α // True } = mk α

@[simp]

theorem Cardinal.mk_eq_mk_of_finite {α β : Type u} [ha : Fintype α] [hb : Fintype β] : mk α = mk β ↔ Fintype.card α = Fintype.card β

@[simp]

theorem nonempty_equiv_subtype_const_true_iff {α β : Type u} : Nonempty (α ≃ { _x : β // True }) ↔ Nonempty (α ≃ β)

theorem Finset.mkRaw_card_eq_set_card_range {α : Type u_1} {β : Type u_2} [ha : Fintype α] {f : α → β} : (mkRaw f).card = (Set.range f).ncard

@[simp]

theorem Fintype.card_set_eq_ncard {α : Type u_1} {s : Set α} [hs : Fintype ↑s] : card ↑s = s.ncard

theorem Finset.card_eq_card_iff_equiv {α β : Type u} {sa : Finset α} {sb : Finset β} : sa.card = sb.card ↔ Nonempty (↥sa ≃ ↥sb)

theorem Set.injOn_of_card_image_eq' {α : Type u_1} {s : Set α} {f : α → α} (h₁ : s.Finite) (h₂ : Cardinal.mk ↑(f '' s) = Cardinal.mk ↑s) : InjOn f s

theorem Set.card_image_eq_iff_injOn' {α : Type u_1} {s : Set α} {f : α → α} (h₁ : s.Finite) : Cardinal.mk ↑(f '' s) = Cardinal.mk ↑s ↔ InjOn f s

theorem Set.ncard_eq_ncard_iff_nonempty_equiv {α β : Type u} {sa : Set α} {sb : Set β} (ha : sa.Finite) (hb : sb.Finite) : sa.ncard = sb.ncard ↔ Nonempty (↑sa ≃ ↑sb)

theorem Set.ncard_image_eq_iff_injOn' {α : Type u_1} {s : Set α} {f : α → α} (h₁ : s.Finite) : (f '' s).ncard = s.ncard ↔ InjOn f s

theorem nonempty_equiv_iff_bijective {α : Type u_1} {β : Type u_2} : Nonempty (α ≃ β) ↔ ∃ (f : α → β), Function.Bijective f

theorem Set.ncard_eq_ncard_iff_bijective {α β : Type u} {sa : Set α} {sb : Set β} (ha : sa.Finite) (hb : sb.Finite) : sa.ncard = sb.ncard ↔ ∃ (f : ↑sa → ↑sb), Function.Bijective f

theorem Set.range_eq_image {α : Type u_1} {β : Type u_2} {f : α → β} : range f = f '' univ

theorem Fintype.card_eq_finset_card {α : Type u_1} [ha : Fintype α] : card α = Finset.univ.card

theorem Set.univ_eq_finset_univ_of_fintype {α : Type u_1} [ha : Fintype α] : univ = ↑Finset.univ

theorem Fintype.card_range_eq_iff_injective {α : Type u_1} {β : Type u_2} [ha : Fintype α] {f : α → β} : card ↑(Set.range f) = card α ↔ Function.Injective f

theorem Fintype.card_eq_set_ncard {α : Type u_1} [ha : Fintype α] : card α = Set.univ.ncard

theorem Set.finite_of_finite_and_bijective {α : Type u_1} {β : Type u_2} {sa : Set α} {sb : Set β} (h₁ : sa.Finite) (h₂ : ∃ (f : ↑sa → ↑sb), Function.Bijective f) : sb.Finite

theorem exi_bijective_symm {α : Type u_1} {β : Type u_2} (h : ∃ (f : α → β), Function.Bijective f) : ∃ (f : β → α), Function.Bijective f

theorem exi_bijective_comm {α : Type u_1} {β : Type u_2} : (∃ (f : α → β), Function.Bijective f) ↔ ∃ (f : β → α), Function.Bijective f

theorem Set.finite_of_finite_and_bijective' {α : Type u_1} {β : Type u_2} {sa : Set α} {sb : Set β} (h₁ : sa.Finite) (h₂ : ∃ (f : ↑sb → ↑sa), Function.Bijective f) : sb.Finite

theorem Set.ncard_image_eq_iff_injOn {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} (h₁ : s.Finite) : (f '' s).ncard = s.ncard ↔ InjOn f s

theorem Set.range_sum_inl_card_eq {α : Type u_1} {β : Type u_2} [ha : Fintype α] : (range Sum.inl).ncard = Fintype.card α

theorem Set.range_sum_inr_card_eq {α : Type u_1} {β : Type u_2} [hb : Fintype β] : (range Sum.inr).ncard = Fintype.card β

theorem Set.nonempty_range_equiv_self_iff_injective {α β : Type u} [ha : Fintype α] {f : α → β} : Nonempty (↑(range f) ≃ α) ↔ Function.Injective f

theorem ncard_eq_card_toFinset {α : Type u_1} [ha : Fintype α] {s : Set α} : s.ncard = s.toFinset.card

theorem ncard_eq_card_toFinset' {α : Type u_1} {s : Set α} [hs : Fintype ↑s] : s.ncard = s.toFinset.card

theorem Set.ncard_eq_cardinal_mk_to_nat {α : Type u_1} {s : Set α} : s.ncard = Cardinal.toNat (Cardinal.mk ↑s)

@[simp]

theorem Cardinal.mk_set_elem {α : Type u_1} {s : Set α} : mk ↑s = mk { x : α // x ∈ s }

@[simp]

theorem Finset.mkRaw_card_eq_fintype_card_iff_injective {α β : Type u} [ha : Fintype α] {f : α → β} : (mkRaw f).card = Fintype.card α ↔ Function.Injective f

@[simp]

theorem Finset.card_le_fintype_card {α : Type u_1} [ha : Fintype α] {s : Finset α} : s.card ≤ Fintype.card α

theorem inf_type : Infinite Type

instance instInfiniteType_projects : Infinite Type

theorem Cardinal.mk_lt_fn_prop {α : Type u_1} : mk α < mk (α → Prop)

theorem nonempty_equiv_of_embed {α : Type u} {β : Type v} (h₁ : Nonempty (α ↪ β)) (h₂ : Nonempty (β ↪ α)) : Nonempty (α ≃ β)

theorem nonempty_embed_trans {α : Type u} {β : Type v} {γ : Type w} (h₁ : Nonempty (α ↪ β)) (h₂ : Nonempty (β ↪ γ)) : Nonempty (α ↪ γ)

theorem nonempty_embed_iff_lift_left {α : Type v} {β : Type w} : Nonempty (α ↪ β) ↔ Nonempty (ULift.{u, v} α ↪ β)

theorem nonempty_embed_iff_lift_right {α : Type v} {β : Type w} : Nonempty (α ↪ β) ↔ Nonempty (α ↪ ULift.{u, w} β)

theorem isEmpty_embed_iff_lift_left {α : Type v} {β : Type w} : IsEmpty (α ↪ β) ↔ IsEmpty (ULift.{u, v} α ↪ β)

theorem isEmpty_embed_iff_lift_right {α : Type v} {β : Type w} : IsEmpty (α ↪ β) ↔ IsEmpty (α ↪ ULift.{u, w} β)

theorem nonempty_embed_iff_lift {α : Type w} {β : Type q} : Nonempty (α ↪ β) ↔ Nonempty (ULift.{u, w} α ↪ ULift.{v, q} β)

theorem isEmpty_embed_iff_lift {α : Type w} {β : Type q} : IsEmpty (α ↪ β) ↔ IsEmpty (ULift.{u, w} α ↪ ULift.{v, q} β)

theorem nonempty_embed_of_empty_embed_rev {α : Type u} {β : Type v} (h : IsEmpty (β ↪ α)) : Nonempty (α ↪ β)

theorem isEmpty_embed_of_isEmpty_of_nonempty {α : Type u} {β : Type v} {γ : Type w} (h₁ : IsEmpty (β ↪ α)) (h₂ : Nonempty (β ↪ γ)) : IsEmpty (γ ↪ α)

@[simp]

theorem isEmpty_set_embed {α : Type u} : IsEmpty (Set α ↪ α)

theorem nonempty_embed_type {α : Type u} : Nonempty (α ↪ Type u)

theorem isEmpty_type_embed {α : Type u} : IsEmpty (Type u ↪ α)

theorem cardinal_embed_type : Nonempty (Cardinal.{u} ↪ Type u)

theorem cardinal_embed_ordinal : Nonempty (Cardinal.{u} ↪ Ordinal.{u})

theorem ifEmpty_embed_trans {α : Type u} {β : Type v} {γ : Type w} (h₁ : IsEmpty (α ↪ β)) (h₂ : IsEmpty (β ↪ γ)) : IsEmpty (α ↪ γ)

@[simp]

theorem nonempty_lift_embed_iff {α : Type v} {β : Type w} : Nonempty (ULift.{u, v} α ↪ β) ↔ Nonempty (α ↪ β)

@[simp]

theorem nonempty_embed_lift_iff {α : Type v} {β : Type w} : Nonempty (α ↪ ULift.{u, w} β) ↔ Nonempty (α ↪ β)

@[simp]

theorem isEmpty_lift_embed_iff {α : Type v} {β : Type w} : IsEmpty (ULift.{u, v} α ↪ β) ↔ IsEmpty (α ↪ β)

@[simp]

theorem isEmpty_embed_lift_iff {α : Type v} {β : Type w} : IsEmpty (α ↪ ULift.{u, w} β) ↔ IsEmpty (α ↪ β)

theorem nonempty_embed_type_max {α : Type v} : Nonempty (α ↪ Type (max v u))

theorem isEmpty_type_max_embed {α : Type v} : IsEmpty (Type (max v u) ↪ α)

@[simp]

theorem type_embed_type_succ : Nonempty (Type u ↪ Type (u + 1))

@[simp]

theorem not_type_succ_embed_type : IsEmpty (Type (u + 1) ↪ Type u)

theorem Finset.card_fin_eq_of {n m : ℕ} {s : Finset (Fin n)} {t : Finset (Fin m)} (hs : ∀ {i : ℕ} {h : i < n}, ⟨i, h⟩ ∈ s → ∃ (h : i < m), ⟨i, h⟩ ∈ t) (ht : ∀ {i : ℕ} {h : i < m}, ⟨i, h⟩ ∈ t → ∃ (h : i < n), ⟨i, h⟩ ∈ s) : s.card = t.card

@[simp]

theorem Equiv.bijective_toFun {α : Type u_1} {β : Type u_2} (e : α ≃ β) : Function.Bijective e.toFun

@[simp]

theorem Equiv.bijective_invFun {α : Type u_1} {β : Type u_2} (e : α ≃ β) : Function.Bijective e.invFun

theorem Set.finite_of_subset_finset {α : Type u_1} {set : Set α} (s : Finset α) (h : ∀ x ∈ set, x ∈ s) : set.Finite

theorem Set.nonempty_infinite_diff_finite {α : Type u_1} {s s' : Set α} (h₁ : s.Infinite) (h₂ : s'.Finite) : (s \ s').Nonempty

theorem Set.nat_exists_le_of_infinite {s : Set ℕ} {n : ℕ} (h : s.Infinite) : ∃ (k : ℕ), n ≤ k ∧ k ∈ s

theorem Set.exists_infinite_preimage_of' {α : Type u_1} {β : Type u_2} [ha : Infinite α] [hb : Finite β] {f : α → β} : ∃ (b : Set β), (f ⁻¹' b).Infinite

theorem Set.exists_infinite_preimage_of {α : Type u_1} {β : Type u_2} [ha : Infinite α] [hb : Finite β] {f : α → β} : ∃ (b : β), (f ⁻¹' {b}).Infinite

theorem Set.infinite_of_subset {α : Type u_1} {s₁ s₂ : Set α} (h₁ : s₂ ⊆ s₁) (h₂ : s₂.Infinite) : s₁.Infinite

theorem Set.exists_infinite_of_forall_exists {α : Type u_1} {β : Type u_2} [ha : Infinite α] [hb : Finite β] {R : α → β → Prop} (h : ∀ (a : α), ∃ (b : β), R a b) : ∃ (b : β), {a : α | R a b}.Infinite

theorem finite_iff_finite_of_bijective {α : Type u_1} {β : Type u_2} (h : ∃ (f : α → β), Function.Bijective f) : Finite α ↔ Finite β

theorem Set.finite_filter_equiv_toFun_iff {α : Type u_1} {β : Type u_2} {p : β → Prop} {e : α ≃ β} : {x : α | p (e x)}.Finite ↔ {y : β | p y}.Finite

theorem Set.finite_filter_equiv_invFun_iff {α : Type u_1} {β : Type u_2} {p : β → Prop} {e : β ≃ α} : {x : α | p (e.invFun x)}.Finite ↔ {y : β | p y}.Finite

theorem Set.finite_filter_equiv_toFun_of {α : Type u_1} {β : Type u_2} {p : β → Prop} {e : α ≃ β} (h : {y : β | p y}.Finite) : {x : α | p (e x)}.Finite

theorem Set.finite_filter_equiv_invFun_of {α : Type u_1} {β : Type u_2} {p : β → Prop} {e : β ≃ α} (h : {y : β | p y}.Finite) : {x : α | p (e.invFun x)}.Finite

theorem Set.finite_filter_of_bijective {α : Type u_1} {β : Type u_2} {p : β → Prop} {f : α → β} (hf : Function.Bijective f) (h : {x : α | p (f x)}.Finite) : {y : β | p y}.Finite

@[simp]

theorem Set.finite_int_abs_le {n : ℤ} : {k : ℤ | |k| ≤ n}.Finite

@[simp]

theorem Set.finite_int_abs_sub_le {c d : ℤ} : {a : ℤ | |a - c| ≤ d}.Finite

@[simp]

theorem Set.finite_toSet_list {α : Type u_1} {xs : List α} : xs.toSet.Finite

@[simp]

instance instFiniteElemToSet {α : Type u_1} {xs : List α} : Finite ↑xs.toSet

theorem Set.ncard_toSet_list_of_nodup {α : Type u_1} {xs : List α} (h : xs.Nodup) : xs.toSet.ncard = xs.length

noncomputable def Set.ncard? {α : Type u_1} (s : Set α) : Option ℕ

Equations

• s.ncard? = if s.Finite then some s.ncard else none

@[simp]

theorem Set.ncard?_empty {α : Type u_1} : ∅.ncard? = some 0

theorem Set.ncard?_image_of_injOn {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} (h : InjOn f s) : (f '' s).ncard? = s.ncard?

theorem Set.ssubset_of {α : Type u_1} {s₁ s₂ : Set α} (x : α) (h₁ : s₁ ⊆ s₂) (h₂ : x ∉ s₁) (h₃ : x ∈ s₂) : s₁ ⊂ s₂

theorem Set.ncard_eq_ite {α : Type u_1} {s : Set α} : s.ncard = have this := Classical.propDecidable; if s.Finite then s.ncard else 0