le_def — Mathlib

English

The order on PartENat is defined by comparing representatives via a witness function h: y.Dom → x.Dom.

Русский

Порядок на PartENat задаётся через представления: x ≤ y эквивалентно существованию отображения h: y.Dom → x.Dom, такое что ∀ hy ∈ y.Dom, x.get(hy) ≤ y.get hy.

LaTeX

$$x \\le y \\iff \\exists h : y.Dom \\to x.Dom, \\forall hy : y.Dom, x.get (h hy) \\le y.get hy$$

Lean4

theorem le_def (x y : PartENat) : x ≤ y ↔ ∃ h : y.Dom → x.Dom, ∀ hy : y.Dom, x.get (h hy) ≤ y.get hy :=
  Iff.rfl

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