English
In a semilattice with bottom, given a nonempty directed set s and a finite set t, if each x in t is below some y in s, then there exists x in s with t.sup id ≤ x.
Русский
В полупорядоченном множестве с нижней границей, если s — не пустое направленное множество и для каждого элемента t⟨x⟩ из t существует y ∈ s с x ≤ y, то найдётся x ∈ s такой, что t.sup id ≤ x.
LaTeX
$$$(\forall x \in t, \exists y \in s, x \le y) \Rightarrow \exists x \in s, t.sup id \le x$$$
Lean4
theorem sup_induction {p : α → Prop} (hb : p ⊥) (hp : ∀ a₁, p a₁ → ∀ a₂, p a₂ → p (a₁ ⊔ a₂)) (hs : ∀ b ∈ s, p (f b)) :
p (s.sup f) := by
induction s using Finset.cons_induction with
| empty => exact hb
| cons _ _ _ ih =>
simp only [sup_cons, forall_mem_cons] at hs ⊢
exact hp _ hs.1 _ (ih hs.2)
