Theorems · Theorem · order theory

iSupIndep_map_orderIso_iff

∀ {ι : Sort u_5} {α : Type u_6} {β : Type u_7} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : α ≃o β)
  {a : ι → α}, iSupIndep (⇑f ∘ a) ↔ iSupIndep a

Defined in

Mathlib.Order.SupIndep

Cited by

5 results in Mathlib

Foundations

Depth 30 from the axioms · uses propext, Quot.sound

Assumes

CompleteLatticeCompleteLattice