addEmptyConstants_symm_isExpansionOn

English

The symmetric expansion by adding an empty constants equivalence provides expansion on M.

Русский

Расширение, полученное обратным преобразованием добавления пустых констант, задаёт расширение на M.

LaTeX

$$$ (LEquiv.addEmptyConstants L (\\emptyset : Set M)).symm.toLHom.IsExpansionOn M $$$

Lean4

instance addEmptyConstants_symm_isExpansionOn : (LEquiv.addEmptyConstants L (∅ : Set M)).symm.toLHom.IsExpansionOn M :=
  LHom.sumElim_isExpansionOn _ _ _

Похожие утверждения