English
Let α be a preorder and s ⊆ α a nonempty finite set. For every a ∈ α with a ∈ s, there exists b ∈ s such that a ≤ b and b is maximal in s.
Русский
Пусть α — предордер, и s ⊆ α — непустое конечное множество. Для каждого a ∈ α, удовлетворяющего a ∈ s, существует b ∈ s such that a ≤ b и b является максимальным в s.
LaTeX
$$$\forall a \in s,\ ∃ b \in s,\ a \le b \wedge \forall c \in s,\ b \ge c.$$$
Lean4
theorem exists_le_maximal (s : Finset α) (ha : a ∈ s) : ∃ b, a ≤ b ∧ Maximal (· ∈ s) b := by
classical
obtain ⟨b, hb, hab, hbmin⟩ : ∃ b ∈ s, a ≤ b ∧ _ := by
simpa [Maximal, and_assoc] using {x ∈ s | a ≤ x}.exists_maximal ⟨a, mem_filter.2 ⟨ha, le_rfl⟩⟩
exact ⟨b, hab, hb, fun c hc hbc ↦ hbmin hc (hab.trans hbc) hbc⟩
