le_coe_iff — Mathlib

English

For every n ∈ ℕ and x ∈ PartENat, (n : PartENat) ≤ x iff there exists h ∈ x.Dom with n ≤ x.get(h).

Русский

Для каждого n ∈ ℕ и x ∈ PartENat, (n : PartENat) ≤ x эквивалентно существованию h ∈ x.Dom с условием n ≤ x.get(h).

LaTeX

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

Lean4

theorem le_coe_iff (x : PartENat) (n : ℕ) : x ≤ n ↔ ∃ h : x.Dom, x.get h ≤ n :=
  by
  change (∃ h : True → x.Dom, _) ↔ ∃ h : x.Dom, x.get h ≤ n
  simp only [forall_prop_of_true, dom_natCast, get_natCast']

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