disjoint_ker_of_nondegenerate_restrict

English

Another restatement of ker-disjointness under nondegenerate restriction.

Русский

Еще одно переформулирование несоприкосновения ядра и подпространства при ограничении.

LaTeX

$$Disjoint_W_ker_B_variant$$

Lean4

theorem disjoint_ker_of_nondegenerate_restrict {B : M →ₗ[R] M →ₗ[R] M₁} {W : Submodule R M}
    (hW : (B.domRestrict₁₂ W W).Nondegenerate) : Disjoint W (LinearMap.ker B) :=
  by
  refine Submodule.disjoint_def.mpr fun x hx hx' ↦ ?_
  let x' : W := ⟨x, hx⟩
  suffices x' = 0 by simpa [x']
  apply hW.1 x'
  simp_rw [Subtype.forall, domRestrict₁₂_apply]
  intro y hy
  rw [mem_ker] at hx'
  simp [x', hx']

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