orthogonal_gc — Mathlib

English

The orthogonal operation establishes a Galois connection between the lattice of subspaces of E and its order dual: K^⊥ ≤ L iff L^⊥ ≤ K.

Русский

Ортогональное дополнение образует Галуа-связь между решетками подпространств E и их порядковым двойником: K^⊥ ≤ L эквивалентно L^⊥ ≤ K.

LaTeX

$$$K^\perp \le L \;\iff\; L^\perp \le K$$$

Lean4

/-- `orthogonal` gives a `GaloisConnection` between
`Submodule 𝕜 E` and its `OrderDual`. -/
theorem orthogonal_gc : @GaloisConnection (Submodule 𝕜 E) (Submodule 𝕜 E)ᵒᵈ _ _ orthogonal orthogonal := fun _K₁ _K₂ =>
  ⟨fun h _v hv _u hu => inner_left_of_mem_orthogonal hv (h hu), fun h _v hv _u hu =>
    inner_left_of_mem_orthogonal hv (h hu)⟩

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