proposition: Lemma preserves_join `{JoinSemiLattice_Morphism L K f} x y : f (x ⊔ y) = f x ⊔ f y.
proof: Proof. Proof preserves_sg_op x y. Lemma preserves_bottom `{BoundedJoinSemiLattice_Morphism L K f} : f ⊥ = ⊥. Proof (preserves_mon_unit (f:=f)). Lemma preserves_meet `{MeetSemiLattice_Morphism L K f} x y : f (x ⊓ y) = f x ⊓ f y. Proof preserves_sg_op x y. Section bounded_join_sl_props. Context `{BoundedJoinSemiLattice L}. Instance join_bottom_l: LeftIdentity (⊔) ⊥ := _. Instance join_bottom_r: RightIdentity (⊔) ⊥ := _. End bounded_join_sl_props. Section lattice_props. Context `{Lattice L}. Definition meet_join_absorption x y : x ⊓ (x ⊔ y) = x := absorption x y. Definition join_meet_absorption x y : x ⊔ (x ⊓ y) = x := absorption x y. End lattice_props. Section distributive_lattice_props. Context `{DistributiveLattice L}. Instance join_meet_distr_l: LeftDistribute (⊔) (⊓). Proof join_meet_distr_l _. Global Instance join_meet_distr_r: RightDistribute (⊔) (⊓). Proof. intros x y z. rewrite !(commutativity _ z). now apply distribute_l. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.theory.groups