lt_coe_iff — Mathlib

English

For a natural number n and x ∈ PartENat, (n : PartENat) < x iff for all h ∈ x.Dom, n < x.get(h).

Русский

Для натурального n и x ∈ PartENat, (n : PartENat) < x тогда и только тогда, когда для всех h ∈ x.Dom выполняется n < x.get(h).

LaTeX

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

Lean4

theorem lt_coe_iff (x : PartENat) (n : ℕ) : x < n ↔ ∃ h : x.Dom, x.get h < n := by
  simp only [lt_def, forall_prop_of_true, get_natCast', dom_natCast]

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