iSupIndep_map_orderIso_iff — Mathlib

English

Independence is preserved and reflected by an order isomorphism.

Русский

Независимость сохраняется и отражается порядковой изоморфией.

LaTeX

$$$\\\\forall ι α β [CompleteLattice α] [CompleteLattice β] (f: OrderIso α β) {a: ι → α}, iSupIndep (f \\circ a) \\\\iff iSupIndep a$$$

Lean4

@[simp]
theorem iSupIndep_map_orderIso_iff {ι : Sort*} {α β : Type*} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β)
    {a : ι → α} : iSupIndep (f ∘ a) ↔ iSupIndep a :=
  ⟨fun h =>
    have hf : f.symm ∘ f ∘ a = a := congr_arg (· ∘ a) f.left_inv.comp_eq_id
    hf ▸ h.map_orderIso f.symm,
    fun h => h.map_orderIso f⟩

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