English
A refined description of the strict order c < a ⨳ b: it is equivalent to the existence of a' < a and b' < b with c ♯ a' ⨳ b' ≤ (a' ⨳ b) ⨳ a ⨳ b'.
Русский
Уточнённое описание строгого порядка c < a ⨳ b: эквивалентно существованию a' < a и b' < b такие, что c ♯ a' ⨳ b' ≤ (a' ⨳ b) ⨳ a ⨳ b'.
LaTeX
$$$\\forall a,b,c \\in \\mathrm{Ordinal},\\ Iff( c < a \\nabla b,\\ Exists a' < a, \\ Exists b' < b,\\ c \\sharp a' \\nabla b' ≤ a' \\nabla b \\sharp a \\nabla b')$$$
Lean4
theorem lt_nmul_iff : c < a ⨳ b ↔ ∃ a' < a, ∃ b' < b, c ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b' :=
by
refine ⟨fun h => ?_, ?_⟩
· rw [nmul] at h
simpa using notMem_of_lt_csInf h ⟨0, fun _ _ => bot_le⟩
· rintro ⟨a', ha, b', hb, h⟩
have := h.trans_lt (nmul_nadd_lt ha hb)
rwa [nadd_lt_nadd_iff_right] at this
