subset — Mathlib

English

If A1 ⊆ A2 and hf is FreimanHom on A2 → B2 with a function hf' : A1 → B1, then hf' gives FreimanHom on A1 → B1.

Русский

Если A1 ⊆ A2 и hf — FreimanHom на A2 → B2, а hf' : A1 → B1, то hf' задаёт FreimanHom на A1 → B1.

LaTeX

$$subset (hA) (hf) (hf') : IsMulFreimanHom n A1 B1 f$$

Lean4

@[to_additive]
theorem subset (hA : A₁ ⊆ A₂) (hf : IsMulFreimanHom n A₂ B₂ f) (hf' : MapsTo f A₁ B₁) : IsMulFreimanHom n A₁ B₁ f
    where
  mapsTo := hf'
  __ := hf.comp (isMulFreimanHom_id hA)

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