English
The dual of a concept lattice is isomorphic to the concept lattice of the dual context.
Русский
Двойственность решётки концептов эквивалентна дуальной концепции контекста.
LaTeX
$$$\text{swapEquiv} : (\text{Concept } α β r)^{\mathrm{op}} \cong_{\!\!\!} \text{Concept } β α (\mathrm{Function.swap}\ r)$$$
Lean4
/-- The dual of a concept lattice is isomorphic to the concept lattice of the dual context. -/
@[simps]
def swapEquiv : (Concept α β r)ᵒᵈ ≃o Concept β α (Function.swap r)
where
toFun := swap ∘ ofDual
invFun := toDual ∘ swap
left_inv := swap_swap
right_inv := swap_swap
map_rel_iff' := swap_le_swap_iff
