isExtreme_sInter — Mathlib

English

If F is nonempty and every B ∈ F is extreme in A, then A is extreme in the intersection of all B ∈ F.

Русский

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

LaTeX

$$$F\neq \emptyset \to (\forall B \in F, IsExtreme 𝕜 A B) \Rightarrow IsExtreme 𝕜 A (\bigcap F)$$$

Lean4

theorem isExtreme_sInter {F : Set (Set E)} (hF : F.Nonempty) (hAF : ∀ B ∈ F, IsExtreme 𝕜 A B) : IsExtreme 𝕜 A (⋂₀ F) :=
  by simpa [sInter_eq_biInter] using isExtreme_biInter hF hAF

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