le_trans — Mathlib

English

Let f, g, h be partial equivalences between structures M and N in a language L. If f ≤ g and g ≤ h, then f ≤ h; i.e., the relation ≤ on partial equivalences is transitive.

Русский

Пусть f, g, h — частичные эквиваленты между структурами M и N в языке L. Если f ≤ g и g ≤ h, тогда следует f ≤ h; то есть отношение ≤ на частичных эквивалентностях транзитивно.

LaTeX

$$$\forall L\ M\ N\ [L\text{ Structure }M]\ [L\text{ Structure }N],\\ \forall f,g,h : M \equiv_p^L N,\ f \le g \rightarrow g \le h \rightarrow f \le h.$$$

Lean4

theorem le_trans (f g h : M ≃ₚ[L] N) : f ≤ g → g ≤ h → f ≤ h :=
  by
  rintro ⟨le_fg, eq_fg⟩ ⟨le_gh, eq_gh⟩
  refine ⟨le_fg.trans le_gh, ?_⟩
  rw [← eq_fg, ← Embedding.comp_assoc (g := g.toEquiv.toEmbedding), ← eq_gh]
  ext
  simp

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