exists_le_minimal — Mathlib

English

Let α be a preorder and s ⊆ α a finite set. If a ∈ s, there exists b ∈ α with b ≤ a and b is minimal in s.

Русский

Пусть α — предордер и s ⊆ α — конечное множество. Тогда для любого a ∈ s существует b ∈ α такой, что b ≤ a и b минимален в s.

LaTeX

$$$\forall a \in s,\ ∃ b \in α,\ b \le a \wedge \text{Minimal}(b ∈ s).$$$

Lean4

theorem exists_le_minimal (hs : s.Finite) (ha : a ∈ s) : ∃ b, b ≤ a ∧ Minimal (· ∈ s) b := by
  lift s to Finset α using hs; exact s.exists_le_minimal ha

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