English
If for directed family K_i of submonoids of M and p a predicate holding at i, then x belongs to the supremum ⨆ i, ⨆ (h: p i), K_i iff there exists i with p i and x ∈ K_i.
Русский
Если для направленного семейства K_i полубадностей по M, и есть предикат p, тогда x принадлежит верхнему пределу ⨆ i, ⨆ (h: p i), K_i в эквиваленте: существует i с p i и x ∈ K_i.
LaTeX
$$$[\text{DirectedOn}]\; (\forall i, p(i)) \Rightarrow (x \in \bigsqcup_i (\bigsqcup_{h: p(i)} K_i) ) \Leftrightarrow \exists i, p(i) \wedge x \in K_i$$$
Lean4
@[to_additive]
theorem mem_biSup_of_directedOn {ι} {p : ι → Prop} {K : ι → Submonoid M} {i : ι} (hp : p i)
(hK : DirectedOn ((· ≤ ·) on K) {i | p i}) {x : M} : x ∈ (⨆ i, ⨆ (_h : p i), K i) ↔ ∃ i, p i ∧ x ∈ K i :=
by
refine ⟨?_, fun ⟨i, hi', hi⟩ ↦ ?_⟩
· suffices x ∈ closure (⋃ i, ⋃ (_ : p i), (K i : Set M)) → ∃ i, p i ∧ x ∈ K i by
simpa only [closure_iUnion, closure_eq (K _)] using this
refine fun hx ↦ closure_induction (fun _ ↦ ?_) ?_ ?_ hx
· simp
· exact ⟨i, hp, (K i).one_mem⟩
· rintro x y _ _ ⟨i, hip, hi⟩ ⟨j, hjp, hj⟩
rcases hK i hip j hjp with ⟨k, hk, hki, hkj⟩
exact ⟨k, hk, mul_mem (hki hi) (hkj hj)⟩
· apply le_iSup (fun i ↦ ⨆ (_ : p i), K i) i
simp [hi, hi']
-- TODO: this section can be generalized to `[SubmonoidClass B M] [CompleteLattice B]`
-- such that `CompleteLattice.LE` coincides with `SetLike.LE`
