Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-17 11:38 f066eb1a

View on Github →

feat(algebra/lie/subalgebra): define lattice structure for Lie subalgebras (#6279) We already have the lattice structure for Lie submodules but not for subalgebras. This is mostly a lightly-edited copy-paste of the corresponding subset of results for Lie submodules that remain true for subalgebras. The results which hold for Lie submodules but not for Lie subalgebras are:

  • sup_coe_to_submodule and mem_sup
  • is_modular_lattice I have also made a few tweaks to bring the structure and naming of Lie subalgebras a little closer to that of Lie submodules.

Estimated changes

added theorem lie_subalgebra.Inf_coe
added theorem lie_subalgebra.Inf_glb
added theorem lie_subalgebra.bot_coe
modified theorem lie_subalgebra.coe_set_eq
added theorem lie_subalgebra.inf_coe
added theorem lie_subalgebra.le_def
modified def lie_subalgebra.map
added theorem lie_subalgebra.mem_bot
deleted theorem lie_subalgebra.mem_coe'
modified theorem lie_subalgebra.mem_coe
added theorem lie_subalgebra.mem_inf
added theorem lie_subalgebra.mem_top
modified theorem lie_subalgebra.range_incl
added theorem lie_subalgebra.top_coe