Theorems · Theorem · order theory

sSupHom.dual_symm_apply_toFun

∀ {α : Type u_2} {β : Type u_3} [inst : SupSet α] [inst_1 : SupSet β] (f : sInfHom αᵒᵈ βᵒᵈ) (a : α),
  (sSupHom.dual.symm f) a = (⇑OrderDual.ofDual ∘ ⇑f ∘ ⇑OrderDual.toDual) a

Defined in

Mathlib.Order.Hom.CompleteLattice

Cited by

0 results in Mathlib

Foundations

Depth 16 from the axioms · uses Quot.sound

Assumes

SupSetSupSet