card_le_of_embedding' — Mathlib

English

If f : α ↪ β is an embedding and Nat.card β = 0 implies Nat.card α = 0, then Nat.card α ≤ Nat.card β.

Русский

Если f : α ↪ β вложено и Nat.card β = 0 ⇒ Nat.card α = 0, то Nat.card α ≤ Nat.card β.

LaTeX

$$$Nat.card(\alpha) \le Nat.card(\beta)$$$

Lean4

/-- If `f` is an embedding, then `Nat.card α ≤ Nat.card β`. We must also assume
  `Nat.card β = 0 → Nat.card α = 0` since `Nat.card` is defined to be `0` for infinite types. -/
theorem card_le_of_embedding' (f : α ↪ β) (h : Nat.card β = 0 → Nat.card α = 0) : Nat.card α ≤ Nat.card β :=
  card_le_of_injective' f.2 h

Похожие утверждения