F : Type ?u.129007
α : Type u_1
β : Type u_2
γ : Type ?u.129016
δ : Type ?u.129019
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
f : α ≃o β
a✝ : ComplementedLattice α
⊢ ComplementedLattice β
F : Type ?u.129007
α : Type u_1
β : Type u_2
γ : Type ?u.129016
δ : Type ?u.129019
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
f : α ≃o β
⊢ ComplementedLattice α → ComplementedLattice β
intro
no goals
F : Type ?u.129007
α : Type u_1
β : Type u_2
γ : Type ?u.129016
δ : Type ?u.129019
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
f : α ≃o β
a✝ : ComplementedLattice α
⊢ ComplementedLattice β
exact f.complementedLattice
F : Type ?u.129007
α : Type u_1
β : Type u_2
γ : Type ?u.129016
δ : Type ?u.129019
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
f : α ≃o β
a✝ : ComplementedLattice β
⊢ ComplementedLattice α
F : Type ?u.129007
α : Type u_1
β : Type u_2
γ : Type ?u.129016
δ : Type ?u.129019
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
f : α ≃o β
⊢ ComplementedLattice β → ComplementedLattice α
intro
no goals
F : Type ?u.129007
α : Type u_1
β : Type u_2
γ : Type ?u.129016
δ : Type ?u.129019
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
f : α ≃o β
a✝ : ComplementedLattice β
⊢ ComplementedLattice α
exact f.symm.complementedLattice