toNonUnitalSubsemiring_mono — Mathlib

English

The map taking a nonunital subring to its corresponding nonunital subsemiring is monotone: if A ≤ B then toNonUnitalSubsemiring(A) ≤ toNonUnitalSubsemiring(B).

Русский

Отображение, переводящее неединичное подполье в соответствующее неединичное подпполе, монотонно по отношению порядка: если A ≤ B, то toNonUnitalSubsemiring(A) ≤ toNonUnitalSubsemiring(B).

LaTeX

$$∀ {A B : NonUnitalSubring R}, A ≤ B → toNonUnitalSubsemiring(A) ≤ toNonUnitalSubsemiring(B)$$

Lean4

@[mono]
theorem toNonUnitalSubsemiring_mono : Monotone (toNonUnitalSubsemiring : NonUnitalSubring R → NonUnitalSubsemiring R) :=
  toNonUnitalSubsemiring_strictMono.monotone

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