carrier_union — Mathlib

English

If each member of a chain of lifts is extendible over its base, then the union lift is extendible (under algebraicity assumptions).

Русский

Если каждый элемент цепи Lift может быть продолжен над своей базой, то их объединение продолжимо над базой (при наличии алгебраических условий).

LaTeX

$$$(\forall \sigma \in c, \sigma.\text{IsExtendible}) \Rightarrow (\text{union } c \; \text{hc}).\text{IsExtendible}$$$

Lean4

theorem carrier_union : (union c hc).carrier = ⨆ i : c, i.1.carrier :=
  le_antisymm (iSup_le <| by rintro ⟨i, rfl | hi⟩; exacts [bot_le, le_iSup_of_le ⟨i, hi⟩ le_rfl]) <|
    iSup_le fun i ↦ le_iSup_of_le ⟨i, .inr i.2⟩ le_rfl

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