Commit 2023-10-12 10:52 6025756d

View on Github →

chore: improve defeq for Sup and sSup of LieSubmodules (#7608) The point is that the following four lemmas are now all true by definition:

LieSubmodule.inf_coe_toSubmodule
LieSubmodule.sInf_coe_toSubmodule
LieSubmodule.sup_coe_toSubmodule [previously existed but not true by definition]
LieSubmodule.sSup_coe_toSubmodule [previously did not exist]

Estimated changes

Modified Mathlib/Algebra/Lie/Submodule.lean

added theorem LieSubmodule.iSup_coe_toSubmodule

added theorem LieSubmodule.iSup_induction'

added theorem LieSubmodule.iSup_induction

added theorem LieSubmodule.mem_iSup_of_mem

added theorem LieSubmodule.sInf_coe_toSubmodule'

deleted theorem LieSubmodule.sInf_glb

added theorem LieSubmodule.sSup_coe_toSubmodule'

added theorem LieSubmodule.sSup_coe_toSubmodule

Modified Mathlib/LinearAlgebra/Finsupp.lean

added theorem Submodule.mem_sSup_iff_exists_finset

Modified Mathlib/LinearAlgebra/Span.lean

added theorem Submodule.mem_sSup