English
If the index set ι is nonempty and S_i is directed by ≤, then x ∈ iSup_i S_i iff ∃ i, x ∈ S_i.
Русский
Если индексное множество не пусто и S_i направлено по отношению ≤, то x ∈ iSup_i S_i тогда и только тогда, когда ∃ i, x ∈ S_i.
LaTeX
$$$$ x \in \big\vee_i S_i \iff \exists i, x \in S_i. $$$$
Lean4
theorem mem_iSup_of_directed {ι : Type*} [hι : Nonempty ι] {S : ι → L.Substructure M} (hS : Directed (· ≤ ·) S)
{x : M} : x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i :=
by
refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩
suffices x ∈ closure L (⋃ i, (S i : Set M)) → ∃ i, x ∈ S i by simpa only [closure_iUnion, closure_eq (S _)] using this
refine fun hx ↦ closure_induction hx (fun _ ↦ mem_iUnion.1) (fun f v hC ↦ ?_)
simp_rw [Set.mem_setOf] at *
have ⟨i, hi⟩ := hS.finite_le (fun i ↦ Classical.choose (hC i))
refine
⟨i, (S i).fun_mem f v (fun j ↦ hi j (Classical.choose_spec (hC j)))⟩
-- This proof uses the fact that `Substructure.closure` is finitary.
