Orthogonality for affine subspaces

Define AffineSubspace.IsOrtho s t as s.direction ⟂ t.direction and develop basic API (mostly copy from
Submodule.IsOrtho). Additions specific to affine subspaces
include lemmas like IsOrtho.trans_parallel.

Define AffineSubspace.orthogonal, e.g., as

/-- Orthogonal complement to an affine subspace passing through a given point. -/
def orthogonal (s : AffineSubspace ℝ P) (b : P) : AffineSubspace ℝ P :=
.comap (AffineMap.id ℝ P -ᵥ AffineMap.const ℝ P b) (s.directionᗮ).toAffineSubspace

and prove lemmas like "orthogonal complements through different
points are parallel", "orthogonal complements to parallel affine
subspaces are parallel" (+ an iff version assuming that the
subspaces are closed).