English
Let α be a type with a transitive relation r and let f : ι → α be a function defined on a nonempty index set ι, together with a directed structure D for r and f. Then for every finite Finset s ⊆ ι, there exists z ∈ α such that for all i ∈ s, r(f(i), f(z)).
Русский
Пусть α – множество с транзитивным отношением r и функция f: ι → α определена на не пустом индексе ι, вместе с направленной структурой r. Тогда для любого конечного подмножества s ⊆ ι существует элемент z ∈ α such that для каждого i ∈ s выполняется r(f(i), f(z)).
LaTeX
$$$\forall s \text{ Finset of } ι, \ \exists z \in α, \ \forall i \in s, \ r(f(i), f(z)).$$$
Lean4
theorem finset_le {r : α → α → Prop} [IsTrans α r] {ι} [hι : Nonempty ι] {f : ι → α} (D : Directed r f) (s : Finset ι) :
∃ z, ∀ i ∈ s, r (f i) (f z) :=
show ∃ z, ∀ i ∈ s.1, r (f i) (f z) from
Multiset.induction_on s.1
(let ⟨z⟩ := hι;
⟨z, fun _ ↦ by simp⟩)
fun i _ ⟨j, H⟩ ↦
let ⟨k, h₁, h₂⟩ := D i j
⟨k, fun _ h ↦ (Multiset.mem_cons.1 h).casesOn (fun h ↦ h.symm ▸ h₁) fun h ↦ _root_.trans (H _ h) h₂⟩
