exists_prop_of_containsZero

Mathlib.CategoryTheory.ObjectProperty.ContainsZero

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

English

If P.ContainsZero holds, there exists Z ∈ C with IsZero Z and P Z.

Русский

Если P.ContainsZero, существует Z в C такое, что IsZero Z и P Z.

LaTeX

$$$$ \exists Z:\, C,\ IsZero(Z) \land P(Z). $$$$

Lean4

theorem exists_prop_of_containsZero [P.ContainsZero] : ∃ (Z : C), IsZero Z ∧ P Z :=
  ContainsZero.exists_zero

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

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

Разделы

Аффилиация

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