exists_le — Mathlib

English

Let α be a nonempty type with a preorder and IsDirected α (≤). For every finite Finset s ⊆ α, there exists M ∈ α such that i ≤ M for all i ∈ s.

Русский

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

LaTeX

$$$\forall s \in \text{Finset } α,\ \exists M \in α,\ \forall i \in s,\ i \le M.$$$

Lean4

theorem exists_le [Nonempty α] [Preorder α] [IsDirected α (· ≤ ·)] (s : Finset α) : ∃ M, ∀ i ∈ s, i ≤ M :=
  directed_id.finset_le _

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