convex_diff — Mathlib

English

If F is a nonempty family of subsets and each B ∈ F is extreme in A, then A is extreme in the intersection over all B ∈ F.

Русский

Если F непустое семейство подмножеств и каждое B ∈ F крайнее в A, то A крайнее в пересечении всех B ∈ F.

LaTeX

$$$F \text{ nonempty} \land (\forall B \in F, IsExtreme 𝕜 A B) \Rightarrow IsExtreme 𝕜 A (\bigcap F)$$$

Lean4

theorem convex_diff [IsOrderedRing 𝕜] (hA : Convex 𝕜 A) (hAB : IsExtreme 𝕜 A B) : Convex 𝕜 (A \ B) :=
  convex_iff_openSegment_subset.2 fun _ ⟨hx₁A, hx₁B⟩ _ ⟨hx₂A, _⟩ _ hx ↦
    ⟨hA.openSegment_subset hx₁A hx₂A hx, fun hxB ↦ hx₁B (hAB.2 hx₁A hx₂A hxB hx)⟩

Похожие утверждения