isExtreme_iInter — Mathlib

English

If every Fi in a nonempty family F is extreme in A, then A is extreme in the intersection of all Fi.

Русский

Если для всей семейства Fi непустого семейства F все Fi являются крайними в A, то A является крайним в пересечении всех Fi.

LaTeX

$$$\forall i,\ IsExtreme 𝕜 A (F_i) \Rightarrow IsExtreme 𝕜 A \bigl(\bigcap_{i} F_i\bigr)$$$

Lean4

theorem isExtreme_iInter {ι : Sort*} [Nonempty ι] {F : ι → Set E} (hAF : ∀ i : ι, IsExtreme 𝕜 A (F i)) :
    IsExtreme 𝕜 A (⋂ i : ι, F i) := by
  inhabit ι
  refine ⟨iInter_subset_of_subset default (hAF default).1, fun x₁ hx₁A x₂ hx₂A x hxF hx ↦ ?_⟩
  rw [mem_iInter] at hxF ⊢
  exact fun i ↦ (hAF i).2 hx₁A hx₂A (hxF i) hx

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