le_isoClosure

Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ObjectProperty.le_isoClosure

English

For every object X, if P holds at X, then X lies in the iso-closure of P.

Русский

Для каждого объекта X, если P(X) верно, то X принадлежит изоморфному замыканию P.

LaTeX

$$$$ \forall X,\; P(X) \Rightarrow isoClosure(P)(X). $$$$

Lean4

theorem le_isoClosure : P ≤ isoClosure P := fun X hX => ⟨X, hX, ⟨Iso.refl X⟩⟩

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

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

Разделы

Аффилиация

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