English
Two partial equivalences f ≤ g are ordered iff there exist dom and cod inclusions with a compatibility condition on their embeddings.
Русский
Пара частичных эквивалентов f ≤ g начинается с существования включений домена и кодома и совместимости вложений.
LaTeX
$$$ f \le g \iff \exists dom\le dom, \exists cod\le cod, \forall x, inclusion cod\le cod (f.toEquiv x) = g.toEquiv (inclusion dom\le dom x) $$$
Lean4
theorem le_iff {f g : M ≃ₚ[L] N} :
f ≤ g ↔
∃ dom_le_dom : f.dom ≤ g.dom,
∃ cod_le_cod : f.cod ≤ g.cod, ∀ x, inclusion cod_le_cod (f.toEquiv x) = g.toEquiv (inclusion dom_le_dom x) :=
by
constructor
· exact fun h ↦ ⟨dom_le_dom h, cod_le_cod h, by intro x; apply (subtype _).inj'; rwa [toEquiv_inclusion_apply]⟩
· rintro ⟨dom_le_dom, le_cod, h_eq⟩
rw [le_def]
exact ⟨dom_le_dom, by ext; change subtype _ (g.toEquiv _) = _; rw [← h_eq]; rfl⟩
