superset

Mathlib.Combinatorics.Additive.FreimanHom

URI: https://scilib.ai/kg/mathlib#IsMulFreimanHom.superset

English

If B1 ⊆ B2, then superset property holds: FreimanHom n A B1 f implies FreimanHom n A B2 f.

Русский

Если B1 ⊆ B2, то FreimanHom на A → B1 f implies FreimanHom на A → B2 f.

LaTeX

$$superset (hB) (hf) : IsMulFreimanHom n A B2 f$$

Lean4

@[to_additive]
theorem superset (hB : B₁ ⊆ B₂) (hf : IsMulFreimanHom n A B₁ f) : IsMulFreimanHom n A B₂ f :=
  (isMulFreimanHom_id hB).comp hf

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

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

Разделы

Аффилиация

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