exists_ge — Mathlib

English

Let α be directed under ≥. For a finite subset s of α, there exists M such that M ≤ i for all i ∈ s.

Русский

Пусть α ориентировано по ≥. Для конечного подмножества s ⊆ α существует M такой, что M ≤ i для всех i ∈ s.

LaTeX

$$$\\\\exists M \\\\in \\\\alpha, \\\\forall i \\\\in s, \\\\ M \\\\le i.$$$

Lean4

theorem exists_ge [IsDirected α (· ≥ ·)] {s : Set α} (hs : s.Finite) : ∃ M, ∀ i ∈ s, M ≤ i :=
  directed_id.finite_set_le (r := (· ≥ ·)) hs

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