exists_le_minimal — Mathlib

English

Let α be a preorder and s ⊆ α a nonempty finite set. For every a ∈ s, there exists b ∈ α with b ≤ a, such that b is minimal with respect to s (i.e., b ∈ s and ∀ c ∈ s, b ≤ c).

Русский

Пусть α — предордер и s ⊆ α конечное непустое множество. Для каждого a ∈ s существует b ∈ α с b ≤ a, при этом b минимален относительно s (то есть b ∈ s и ∀ c ∈ s, b ≤ c).

LaTeX

$$$\exists b \in s,\ b \le a \wedge \forall c \in s,\ b \le c.$$$

Lean4

theorem exists_le_minimal (s : Finset α) (ha : a ∈ s) : ∃ b ≤ a, Minimal (· ∈ s) b :=
  exists_le_maximal (α := αᵒᵈ) s ha

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