mem_biSup_of_directedOn — Mathlib

English

For a directed family K: ι → Subsemigroup M and a predicate p on ι, x belongs to the biSup ⨆ i ⨆ (_h : p i), K i iff there exists i with p i and x ∈ K i.

Русский

Для направленного семейства K: ι → Subsemigroup M и предиката p на ι, x ∈ ⨆ i ⨆ (h : p i), K i тогда и только тогда существует i, такое что p i и x ∈ K i.

LaTeX

$$$ x \in \big(\bigsup i, \bigsup (\\_h : p i), K i\\big) \iff \exists i, p i \land x \in K i $$$

Lean4

@[to_additive]
theorem mem_biSup_of_directedOn {ι} {p : ι → Prop} {K : ι → Subsemigroup M} (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
    · 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 `[MulMemClass B M] [CompleteLattice B]`
      -- such that `complete_lattice.le` coincides with `set_like.le`

Похожие утверждения