exists_minimalFor — Mathlib

English

For a map f: ι → α and s ⊆ ι with (f''s) PWO, there exists i ∈ s with f(i) minimal on s.

Русский

Для отображения f: ι → α и подмножества s ⊆ ι, если f''s частично хорошо упорядочено, существует i ∈ s такая, что f(i) минимально на s.

LaTeX

$$$f:\\{ι\\to α\\},\\; s:\\text{Set } ι,\\; (f''s).IsPWO \\Rightarrow \\exists i \\in s, \\ MinimalFor(\\cdot \\in s) f i$$$

Lean4

theorem exists_minimalFor (f : ι → α) (s : Set ι) (h : (f '' s).IsPWO) (hs : s.Nonempty) :
    ∃ i, MinimalFor (· ∈ s) f i := by
  obtain ⟨_, h⟩ := h.exists_minimal (hs.image _)
  obtain ⟨a, ha, rfl⟩ := h.1
  exact ⟨a, ha, fun b hb => h.2 (mem_image_of_mem _ hb)⟩

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