feat(Convex): visibility through a set

[YaelDillies]

Define the relation of visibility with respect to a set, and lower bound how many elements of a set a point sees in terms of the dimension of that set.

This will be used to prove a sort of strengthening of Freiman's lemma in additive combinatorics.

From LeanCamCombi

---

[github-actions]

PR summary a77a8512a5

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Analysis.Convex.Visible	1356

---

Declarations diff

+ IsClosed.convexHull_subset_affineSpan_isVisible
+ IsClosed.exists_wbtw_isVisible
+ IsOpen.eq_of_isVisible_of_left_mem
+ IsVisible
+ IsVisible.eq_of_mem_interior
+ IsVisible.mem_convexHull_isVisible
+ IsVisible.mono
+ IsVisible.of_convexHull_of_pos
+ IsVisible.rfl
+ isVisible_comm
+ isVisible_iff_lineMap
+ rank_le_card_isVisible
+ ⟨IsVisible.symm,

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[b-mehta]

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by b-mehta.