comap — Mathlib

English

The map after comap is contained in the original subspace: (s.comap f).map f ≤ s.

Русский

Образ после обратного образа содержится в исходном подпроизвольстве: (s.comap f).map f ≤ s.

LaTeX

$$$ (s.comap f).map f \\le s $$$

Lean4

/-- The preimage of an affine subspace under an affine map as an affine subspace. -/
def comap (f : P₁ →ᵃ[k] P₂) (s : AffineSubspace k P₂) : AffineSubspace k P₁
    where
  carrier := f ⁻¹' s
  smul_vsub_vadd_mem t p₁ p₂ p₃ (hp₁ : f p₁ ∈ s) (hp₂ : f p₂ ∈ s)
    (hp₃ :
      f p₃ ∈
        s) :=
    show f _ ∈ s by
      rw [AffineMap.map_vadd, LinearMap.map_smul, AffineMap.linearMap_vsub]
      apply s.smul_vsub_vadd_mem _ hp₁ hp₂ hp₃

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