coe_le_iff — Mathlib

English

For any natural n and x ∈ PartENat, (n : PartENat) ≤ x iff ∀ h ∈ x.Dom, n ≤ x.get(h).

Русский

Для любого натурального n и x ∈ PartENat, (n : PartENat) ≤ x эквивалентно ∀ h ∈ x.Dom, n ≤ x.get(h).

LaTeX

$$$ (n : \mathrm{PartENat}) \le x \iff \forall h : x.Dom, n \le x.get(h) $$$

Lean4

theorem coe_le_iff (n : ℕ) (x : PartENat) : (n : PartENat) ≤ x ↔ ∀ h : x.Dom, n ≤ x.get h :=
  by
  rw [← some_eq_natCast]
  simp only [le_def, exists_prop_of_true, dom_some, forall_true_iff]
  rfl

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