English
Two lifts satisfy a strict order relation iff there exists an inclusion from L1 to L2 compatible with their embeddings, i.e. L2 embeds after including L1 equals L1’s embedding.
Русский
Два Lift удовлетворяют строгому отношению порядка эквивалентно существованию включения из L1 в L2, совместимого с их вложениями: вложение L2 после включения равно вложению L1.
LaTeX
$$$L_1 < L_2 \iff \exists h: L_1.\operatorname{carrier} \lt L_2.\operatorname{carrier},\; L_2.\text{emb} \circ (\text{inclusion } h) = L_1.\text{emb}$$$
Lean4
theorem lt_iff : L₁ < L₂ ↔ ∃ h : L₁.carrier < L₂.carrier, L₂.emb.comp (inclusion h.le) = L₁.emb :=
by
rw [lt_iff_le_carrier_ne, le_iff]
exact ⟨fun h ↦ ⟨h.1.1.lt_of_ne h.2, h.1.2⟩, fun h ↦ ⟨⟨h.1.le, h.2⟩, h.1.ne⟩⟩
