isoClosure_le_iff — Mathlib

English

For any P and Q, if Q is closed under isomorphisms, then isoClosure(P) ≤ Q if and only if P ≤ Q.

Русский

Для любых P и Q, если Q замкнуто по изоморфизмам, то isoClosure(P) ≤ Q тогда и только тогда, когда P ≤ Q.

LaTeX

$$$$ [Q.IsClosedUnderIsomorphisms] \Rightarrow (isoClosure(P) \le Q \ \iff \ P \le Q). $$$$

Lean4

theorem isoClosure_le_iff [IsClosedUnderIsomorphisms Q] : isoClosure P ≤ Q ↔ P ≤ Q :=
  ⟨(le_isoClosure P).trans, fun h => (monotone_isoClosure h).trans (by rw [isoClosure_eq_self])⟩

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