mfld_cfg

Mathlib.Logic.Equiv.PartialEquiv

URI: https://scilib.ai/kg/mathlib#mfld_cfg

Lean4

/-- Common `@[simps]` configuration options used for manifold-related declarations. -/
@[deprecated "Use `@[simps (attr := mfld_simps) -fullyApplied]` instead" (since := "2025-09-23")]
def mfld_cfg : Simps.Config where fullyApplied := false

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru