encard_le_coe_iff — Mathlib

English

For any natural k, encard(s) ≤ k holds if and only if s is finite and there exists n with encard(s) = n and n ≤ k.

Русский

Для любого k ∈ ℕ, encard(s) ≤ k эквивалентно тому, что S конечно и существует n ∈ ℕ с encard(s) = n и n ≤ k.

LaTeX

$$$s.encard \le k \iff \bigl( \operatorname{Finite}(s) \land \exists n_0 \in \mathbb{N},\ s.encard = n_0 \land n_0 \le k \bigr)$$$

Lean4

theorem encard_le_coe_iff {k : ℕ} : s.encard ≤ k ↔ s.Finite ∧ ∃ (n₀ : ℕ), s.encard = n₀ ∧ n₀ ≤ k :=
  ⟨fun h ↦ ⟨finite_of_encard_le_coe h, by rwa [ENat.le_coe_iff] at h⟩, fun ⟨_, ⟨n₀, hs, hle⟩⟩ ↦ by
    rwa [hs, Nat.cast_le]⟩

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