extremePoints_pi — Mathlib

English

For a family of sets s(i), the extreme points of the product over all i equal the product of the extreme points at each i: extremePoints(⋯) = ⋯

Русский

Для семейства множеств s(i) крайние точки произведения совпадают с произведением крайних точек по каждому индексу.

LaTeX

$$$\operatorname{extremePoints}_{𝕜}(\mathrm{univ} \cap \pi s) = \mathrm{univ} \cap \pi (i \mapsto \operatorname{extremePoints}_{𝕜}(s(i)))$$$

Lean4

@[simp]
theorem extremePoints_pi (s : ∀ i, Set (M i)) : (univ.pi s).extremePoints 𝕜 = univ.pi fun i ↦ (s i).extremePoints 𝕜 :=
  by
  classical
  ext x
  simp only [mem_extremePoints_iff_left, mem_univ_pi, @forall_and ι]
  refine and_congr_right fun hx ↦ ⟨fun h i ↦ ?_, fun h ↦ ?_⟩
  · rintro x₁ hx₁ x₂ hx₂ hi
    rw [← update_self i x₁ x, h (update x i x₁) _ (update x i x₂)]
    · rintro j
      obtain rfl | hji := eq_or_ne j i <;> simp [*]
    · rw [← Pi.image_update_openSegment]
      exact ⟨_, hi, update_eq_self _ _⟩
    · rintro j
      obtain rfl | hji := eq_or_ne j i <;> simp [*]
  · rintro x₁ hx₁ x₂ hx₂ ⟨a, b, ha, hb, hab, rfl⟩
    ext i
    exact h _ _ (hx₁ _) _ (hx₂ _) ⟨a, b, ha, hb, hab, rfl⟩

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