English
Specialized simplifications of the directed supremum lemma; they express trivial logical consequences of the general statement (e.g., True, False cases).
Русский
Упрощённые следствия общего леммы о направленном супремуме; отражают тривиальные логические выводы (True/False).
LaTeX
$$$\forall a, \text{True}$$$
Lean4
theorem sup_le_of_le_directed {α : Type*} [SemilatticeSup α] [OrderBot α] (s : Set α) (hs : s.Nonempty)
(hdir : DirectedOn (· ≤ ·) s) (t : Finset α) : (∀ x ∈ t, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, t.sup id ≤ x := by
classical
induction t using Finset.induction_on with
| empty =>
simpa only [forall_prop_of_true, and_true, forall_prop_of_false, bot_le, not_false_iff, sup_empty, forall_true_iff,
notMem_empty]
| insert a r _ ih =>
intro h
have incs : (r : Set α) ⊆ ↑(insert a r) := by
rw [Finset.coe_subset]
apply Finset.subset_insert
obtain ⟨x, ⟨hxs, hsx_sup⟩⟩ := ih fun x hx => h x <| incs hx
obtain ⟨y, hys, hay⟩ :=
h a
(Finset.mem_insert_self a r)
-- z ∈ s is above x and y
obtain ⟨z, hzs, ⟨hxz, hyz⟩⟩ := hdir x hxs y hys
use z, hzs
rw [sup_insert, id, sup_le_iff]
exact
⟨le_trans hay hyz, le_trans hsx_sup hxz⟩
-- If we acquire sublattices
-- the hypotheses should be reformulated as `s : SubsemilatticeSupBot`
