multiplicativeClosure_monotone — Mathlib

English

For any W, W' with W' multiplicative, multiplicativeClosure W ≤ W' iff W ≤ W'.

Русский

Для любых W, W' с W' мультипликативным, равенство: multiplicativeClosure(W) ≤ W' тогда и только тогда, когда W ≤ W'.

LaTeX

$$$multiplicativeClosure\,W \le W' \iff W \le W'$$$

Lean4

theorem multiplicativeClosure_monotone : Monotone (multiplicativeClosure (C := C)) := fun _ W' h ↦ by
  simpa using h.trans W'.le_multiplicativeClosure

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