chore(analysis/convex/extreme): Make arguments semi-implicit (#14698)
chore(analysis/convex/extreme): Make arguments semi-implicit (#14698)

Change the definition of `is_extreme` from
```
B ⊆ A ∧ ∀ x₁ x₂ ∈ A, ∀ x ∈ B, x ∈ open_segment 𝕜 x₁ x₂ → x₁ ∈ B ∧ x₂ ∈ B
```
to
```
B ⊆ A ∧ ∀ ⦃x₁⦄, x₁ ∈ A → ∀ ⦃x₂⦄, x₂ ∈ A → ∀ ⦃x⦄, x ∈ B → x ∈ open_segment 𝕜 x₁ x₂ → x₁ ∈ B ∧ x₂ ∈ B
```
and similar for `extreme_points`.





leanprover-community/mathlib,leanprover-community/mathlib