u_biSup_of_lu_eq_self — Mathlib

English

Let gi be a Galois Coinsertion; for f: ∀ i (p i) → α with hf: ∀ i hi, u(l(f(i, hi))) = f(i, hi), then u of the dependent inf is the dependent inf of u-images.

Русский

Пусть gi — Галуа-коинсерция; при f(i, hi) ∈ α и hf: u(l(f(i, hi))) = f(i, hi) имеем равенство.

LaTeX

$$$$ u\left( \bigwedge_{i} \bigwedge_{h i} l(f(i, hi)) \right) = \bigwedge_{i} \bigwedge_{h i} u\big(l(f(i, hi))\big). $$$$

Lean4

theorem u_biSup_of_lu_eq_self [CompleteLattice α] [CompleteLattice β] (gi : GaloisCoinsertion l u) {ι : Sort x}
    {p : ι → Prop} (f : ∀ (i) (_ : p i), β) (hf : ∀ i hi, l (u (f i hi)) = f i hi) :
    u (⨆ (i) (hi), f i hi) = ⨆ (i) (hi), u (f i hi) :=
  gi.dual.l_biInf_of_ul_eq_self _ hf

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