mono

Mathlib.Topology.Bornology.Absorbs

URI: https://scilib.ai/kg/mathlib#Absorbs.mono

English

If s1 is absorbed by t1, and s1 ⊆ s2 while t2 ⊆ t1, then s2 is absorbed by t2.

Русский

Если s1 поглощается t1 и s1 ⊆ s2, а t2 ⊆ t1, то s2 поглощается t2.

LaTeX

$$$Absorbs M s_1 t_1 \rightarrow (s_1 \subseteq s_2) \rightarrow (t_2 \subseteq t_1) \rightarrow Absorbs M s_2 t_2$$$

Lean4

theorem mono (h : Absorbs M s₁ t₁) (hs : s₁ ⊆ s₂) (ht : t₂ ⊆ t₁) : Absorbs M s₂ t₂ :=
  (h.mono_left hs).mono_right ht

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru