coe_lt_iff — Mathlib

English

For any natural number 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}) < x \iff \forall h : x.Dom, n < x.get(h) $$$

Lean4

theorem coe_lt_iff (n : ℕ) (x : PartENat) : (n : PartENat) < x ↔ ∀ h : x.Dom, n < x.get h :=
  by
  rw [← some_eq_natCast]
  simp only [lt_def, exists_prop_of_true, dom_some]
  rfl

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