mono_right — Mathlib

English

Let M be a Bornology on α with a compatible SMul action. If s is absorbed by t1, and t2 is a subset of t1, then s is absorbed by t2.

Русский

Пусть M — били Bornology на α с совместным действием. Если s поглощается t1 относительно M, и t2 ⊆ t1, то s поглощается t2.

LaTeX

$$$Absorbs M s t_1 \rightarrow (t_2 \subseteq t_1) \rightarrow Absorbs M s t_2$$$

Lean4

theorem mono_right (h : Absorbs M s t₁) (ht : t₂ ⊆ t₁) : Absorbs M s t₂ :=
  h.mono fun _ ↦ ht.trans

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