closure_iSup_closure — Mathlib

English

A closure operator commutes with iSup: c(⨆ i, c(f(i))) = c(⨆ i, f(i)).

Русский

Замыкатель commuting с iSup: c(⊔ i, c(f(i))) = c(⊔ i, f(i)).

LaTeX

$$$\\\\forall {\\\\alpha : Type*} [CompleteLattice {\\\\alpha}] (c : ClosureOperator {\\\\alpha}) {f : ι \\\\to {\\\\alpha}}, c (\\\\bigvee i, c (f i)) = c (\\\\bigvee i, f i)$$$

Lean4

@[simp]
theorem closure_iSup_closure (f : ι → α) : c (⨆ i, c (f i)) = c (⨆ i, f i) :=
  le_antisymm (le_closure_iff.1 <| iSup_le fun i => c.monotone <| le_iSup f i) <|
    c.monotone <| iSup_mono fun _ => c.le_closure _

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