English
Let x,y ∈ PartENat. Then x < y if and only if there exists hx ∈ Dom(x) such that for all hy ∈ Dom(y), x.get(hx) < y.get(hy).
Русский
Пусть x,y ∈ PartENat. Тогда x < y тогда и только тогда, когда существует hx ∈ Dom(x), такое что для всех hy ∈ Dom(y) выполняется x.get(hx) < y.get(hy).
LaTeX
$$$ x < y \iff \exists h_x: x.Dom, \forall h_y: y.Dom, x.get(h_x) < y.get(h_y) $$$
Lean4
theorem lt_def (x y : PartENat) : x < y ↔ ∃ hx : x.Dom, ∀ hy : y.Dom, x.get hx < y.get hy :=
by
rw [lt_iff_le_not_ge, le_def, le_def, not_exists]
constructor
· rintro ⟨⟨hyx, H⟩, h⟩
by_cases hx : x.Dom
· use hx
intro hy
specialize H hy
specialize h fun _ => hy
rw [not_forall] at h
cutsat
· specialize h fun hx' => (hx hx').elim
rw [not_forall] at h
obtain ⟨hx', h⟩ := h
exact (hx hx').elim
· rintro ⟨hx, H⟩
exact ⟨⟨fun _ => hx, fun hy => (H hy).le⟩, fun hxy h => not_lt_of_ge (h _) (H _)⟩
