mono

Mathlib.Topology.DiscreteQuotient

URI: https://scilib.ai/kg/mathlib#DiscreteQuotient.LEComap.mono

English

If LEComap f A B holds, and A' ≤ A and B ≤ B', then LEComap f A' B' holds.

Русский

Если LEComap f A B выполняется, и A' ⊆ A, B ⊆ B', то LEComap f A' B' выполняется.

LaTeX

$$$$\\mathrm{LEComap}(f, A, B) \\to A' \\le A \\to B \\le B' \\to \\mathrm{LEComap}(f, A', B').$$$$

Lean4

@[mono]
theorem mono (h : LEComap f A B) (hA : A' ≤ A) (hB : B ≤ B') : LEComap f A' B' :=
  hA.trans <| h.trans <| comap_mono _ hB

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

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

Разделы

Аффилиация

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