English
If a directed family of lifts is bounded above by σ, then the carrier of σ dominates the union of the carriers of the family.
Русский
Если направленная совокупность Lift ограничена сверху генератором σ, то носитель σ доминирует объединение носителей элементов семейства.
LaTeX
$$$\forall i, (\rho_i \le \sigma) \implies \sigma.\operatorname{carrier} \ge \bigcup_i (\rho_i.\operatorname{carrier})$$$
Lean4
theorem le_of_carrier_le_iSup {ι} {ρ : ι → Lifts F E K} {σ τ : Lifts F E K} (hσ : ∀ i, ρ i ≤ σ) (hτ : ∀ i, ρ i ≤ τ)
(carrier_le : σ.carrier ≤ ⨆ i, (ρ i).carrier) : σ ≤ τ :=
le_iff.mpr
⟨carrier_le.trans (iSup_le fun i ↦ (hτ i).1),
algHom_ext_of_eq_adjoin _ (carrier_le.antisymm (iSup_le fun i ↦ (hσ i).1) |>.trans <| iSup_eq_adjoin _ _)
fun x hx ↦
have ⟨i, hx⟩ := Set.mem_iUnion.mp hx
((hτ i).2 ⟨x, hx⟩).trans ((hσ i).2 ⟨x, hx⟩).symm⟩
