mathlib

7958e7da - 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`.