English
Composing an independent indexed family with an order isomorphism preserves independence.
Русский
Сохранение независимости при композиции с порядковой изоморфией.
LaTeX
$$$\\\\forall ι a b, [CompleteLattice α] [CompleteLattice β]\\\\ (f: α \\simeq_o β) \\\\cdot iSupIndep a \\\\Rightarrow iSupIndep (f \\circ a)$$$
Lean4
/-- Composing an independent indexed family with an order isomorphism on the elements results in
another independent indexed family. -/
theorem map_orderIso {ι : Sort*} {α β : Type*} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) {a : ι → α}
(ha : iSupIndep a) : iSupIndep (f ∘ a) := fun i => ((ha i).map_orderIso f).mono_right (f.monotone.le_map_iSup₂ _)
