feat(LinearAlgebra/AffineSpace/AffineSubspace/Basic): map_inf lemmas (#32015)

Add two lemmas about affine maps applied to the infimum of two subspaces, similar to lemmas that exist for various other subobject types.

```lean
lemma map_inf_le (s₁ s₂ : AffineSubspace k P₁) : (s₁ ⊓ s₂).map f ≤ s₁.map f ⊓ s₂.map f :=
```

```lean
lemma map_inf_eq (hf : Function.Injective f) (s₁ s₂ : AffineSubspace k P₁) :
    (s₁ ⊓ s₂).map f = s₁.map f ⊓ s₂.map f := by
```

Author: jsm28

Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean

@@ -561,6 +561,15 @@ theorem map_span (s : Set P₁) : (affineSpan k s).map f = affineSpan k (f '' s)
 theorem map_mono {s₁ s₂ : AffineSubspace k P₁} (h : s₁ ≤ s₂) : s₁.map f ≤ s₂.map f :=
   Set.image_mono h
 
+lemma map_inf_le (s₁ s₂ : AffineSubspace k P₁) : (s₁ ⊓ s₂).map f ≤ s₁.map f ⊓ s₂.map f :=
+  le_inf (map_mono _ inf_le_left) (map_mono _ inf_le_right)
+
+lemma map_inf_eq (hf : Function.Injective f) (s₁ s₂ : AffineSubspace k P₁) :
+    (s₁ ⊓ s₂).map f = s₁.map f ⊓ s₂.map f := by
+  ext p
+  simp [mem_inf_iff]
+  grind
+
 lemma map_mk' (p : P₁) (direction : Submodule k V₁) :
     (mk' p direction).map f = mk' (f p) (direction.map f.linear) := by
   ext q