eq_top_of_restrict_nondegenerate_of_orthogonal_eq_bot

English

The restriction of a reflexive, nondegenerate B to the orthogonal of the span of a singleton x is nondegenerate provided x is not self-orthogonal.

Русский

Ограничение рефлексивной, недегнерированной B к ортогонали(span{x}) недегнерировано, если x не самoортогонален.

LaTeX

$$restrict_nondegenerate_orthogonal_spanSingleton B b₁ b₂ {x} hx : Nondegenerate (B.restrict (B.orthogonal (K ∙ x)))$$

Lean4

theorem eq_top_of_restrict_nondegenerate_of_orthogonal_eq_bot (b₁ : B.IsRefl) (b₂ : (B.restrict W).Nondegenerate)
    (b₃ : B.orthogonal W = ⊥) : W = ⊤ :=
  by
  have := (B.isCompl_orthogonal_of_restrict_nondegenerate b₁ b₂).sup_eq_top
  rwa [b₃, sup_bot_eq] at this

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