closure_iSup₂_closure — Mathlib

English

Similarly for two-parameter iSup: c(⨆ i, j, c(f(i,j))) = c(⨆ i, j, f(i,j)).

Русский

Аналогично двумерному iSup: c(⊔ i,j, c(f(i,j))) = c(⊔ i,j, f(i,j)).

LaTeX

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

Lean4

@[simp]
theorem closure_iSup₂_closure (f : ∀ i, κ i → α) : c (⨆ (i) (j), c (f i j)) = c (⨆ (i) (j), f i j) :=
  le_antisymm (le_closure_iff.1 <| iSup₂_le fun i j => c.monotone <| le_iSup₂ i j) <|
    c.monotone <| iSup₂_mono fun _ _ => c.le_closure _

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