linear_aux — Mathlib

English

The directional constraint of the restricted map is governed by the linear map restriction induced by φ.

Русский

Направляющее ограничение ограниченного отображения управляется линейным отображением, индуцируемым φ.

LaTeX

$$$ E.direction \\le F.direction.comap \\phi.linear $$$

Lean4

theorem linear_aux {φ : P₁ →ᵃ[k] P₂} {E : AffineSubspace k P₁} {F : AffineSubspace k P₂} (hEF : E.map φ ≤ F) :
    E.direction ≤ F.direction.comap φ.linear :=
  by
  rw [← Submodule.map_le_iff_le_comap, ← AffineSubspace.map_direction]
  exact AffineSubspace.direction_le hEF

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