rfl

Mathlib.Order.Bounds.Basic

URI: https://scilib.ai/kg/mathlib#IsCoinitialFor.rfl

English

For any set s, IsCoinitialFor(s,s) holds.

Русский

Для любого множества s выполняется IsCoinitialFor(s,s).

LaTeX

$$$$ IsCoinitialFor(s,s). $$$$

Lean4

@[refl]
protected theorem rfl : IsCoinitialFor s s :=
  .of_subset .rfl

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

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

Разделы

Аффилиация

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