English
Let α and β be complete lattices and l: α → β, u: β → α form a Galois insertion. Then for any index type ι, any predicate p on ι, and any family f with f(i, h) ∈ β for h witnesses p(i), we have l of the dependent supremum of u(f(i, h)) equals the dependent supremum of f(i, h): l( ⨆ i (hi), u(f(i, hi)) ) = ⨆ i (hi), f(i, hi).
Русский
Пусть α и β — полные решетки, и l: α → β, u: β → α образуют Галуа-вставку. Тогда для любого типа индексов ι, для любого предиката p на ι и любой семейства f с f(i, h) ∈ β для любого доказательства h, имеем: l( ⨆ i (hi), u(f(i, hi)) ) = ⨆ i (hi), f(i, hi).
LaTeX
$$$$ l\left( \bigvee_{i:\iota}\; \bigvee_{h:\, p(i)} u\big(f(i,h)\big) \right) = \bigvee_{i:\iota}\; \bigvee_{h:\, p(i)} f(i,h). $$$$
Lean4
theorem l_biSup_u [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) {ι : Sort x} {p : ι → Prop}
(f : ∀ i, p i → β) : l (⨆ (i) (hi), u (f i hi)) = ⨆ (i) (hi), f i hi := by simp only [iSup_subtype', gi.l_iSup_u]
