isExtreme_biInter — 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} \to IsExtreme 𝕜 A (\bigcap_{B\in F} B)$ given $\forall B \in F, IsExtreme 𝕜 A B$$$

Lean4

theorem isExtreme_biInter {F : Set (Set E)} (hF : F.Nonempty) (hA : ∀ B ∈ F, IsExtreme 𝕜 A B) :
    IsExtreme 𝕜 A (⋂ B ∈ F, B) := by
  haveI := hF.to_subtype
  simpa only [iInter_subtype] using isExtreme_iInter fun i : F ↦ hA _ i.2

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