union — Mathlib

English

If a family of lifts is indexed by I and σ is a bound, then σ is below the directed supremum of carriers, hence the lift order respects iSup over carriers.

Русский

Если семейство Lift индуцируется по индексу I, а σ ограничено, то σ ≤ iSup, носители которого — карьеры членов семьи.

LaTeX

$$$\forall i, \rho_i \le \sigma, \left(\bigvee_i (\rho_i.\operatorname{carrier})\right) \le \sigma.\operatorname{carrier} \Rightarrow \sigma \le \tau$$$

Lean4

/-- The union of a chain of lifts. -/
noncomputable def union : Lifts F E K :=
  let t (i : ↑(insert ⊥ c)) := i.val.carrier
  have hc := hc.insert fun _ _ _ ↦ .inl bot_le
  have dir : Directed (· ≤ ·) t := hc.directedOn.directed_val.mono_comp _ fun _ _ h ↦ h.1
  ⟨iSup t,
    (Subalgebra.iSupLift (toSubalgebra <| t ·) dir (·.val.emb)
          (fun i j h ↦
            AlgHom.ext fun x ↦
              (hc.total i.2 j.2).elim (fun hij ↦ (hij.snd x).symm) fun hji ↦
                by
                rw [AlgHom.comp_apply, ← inclusion]
                dsimp only [coe_type_toSubalgebra]
                rw [← hji.snd (inclusion h x), inclusion_inclusion, inclusion_self, AlgHom.id_apply x])
          _ rfl).comp
      (Subalgebra.equivOfEq _ _ <| toSubalgebra_iSup_of_directed dir)⟩

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