encard_le_coe_iff_finite_ncard_le

English

For natural k, encard s ≤ k iff s is finite and s.ncard ≤ k.

Русский

Для натурального k encard s ≤ k тогда и только тогда, когда s конечно и s.ncard ≤ k.

LaTeX

$$$ s.encard \\le k \\iff s.Finite \\land s.ncard \\le k $$$

Lean4

theorem encard_le_coe_iff_finite_ncard_le {k : ℕ} : s.encard ≤ k ↔ s.Finite ∧ s.ncard ≤ k :=
  by
  rw [encard_le_coe_iff, and_congr_right_iff]
  exact fun hfin ↦
    ⟨fun ⟨n₀, hn₀, hle⟩ ↦ by rwa [ncard_def, hn₀, ENat.toNat_coe], fun h ↦ ⟨s.ncard, by rw [hfin.cast_ncard_eq], h⟩⟩

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