monotone_retractClosure — Mathlib

English

If P ≤ Q for object properties P and Q, then retractClosure P ≤ retractClosure Q.

Русский

Если P ⊆ Q для свойств объектов P и Q, то retractClosure(P) ⊆ retractClosure(Q).

LaTeX

$$$P \le Q \Rightarrow \operatorname{retractClosure}(P) \le \operatorname{retractClosure}(Q)$$$

Lean4

theorem monotone_retractClosure (h : P ≤ Q) : retractClosure P ≤ retractClosure Q :=
  by
  rintro X ⟨X', hX', ⟨e⟩⟩
  exact ⟨X', h _ hX', ⟨e⟩⟩

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