orthogonal_eq_top_iff — Mathlib

English

For reflexive B, the condition B.orthogonal W equals ⊥ or ⊤ is equivalent to W being ⊥ or ⊤ respectively under nondegeneracy of restrictions.

Русский

Для рефлексивной B равенство B.orthogonal W с ⊥ или ⊤ эквивалентно W = ⊥ или W = ⊤ соответственно при недегенерации ограничений.

LaTeX

$$B.IsRefl → (B.restrict W).Nondegenerate → (B.orthogonal W = ⊥) ↔ (W = ⊤)$$

Lean4

theorem orthogonal_eq_top_iff (b₁ : B.IsRefl) (b₂ : (B.restrict W).Nondegenerate) : B.orthogonal W = ⊤ ↔ W = ⊥ :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
  have := (B.isCompl_orthogonal_of_restrict_nondegenerate b₁ b₂).inf_eq_bot
  rwa [h, inf_top_eq] at this

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