fromRel_bot

Mathlib.Data.Sym.Sym2

URI: https://scilib.ai/kg/mathlib#Sym2.fromRel_bot

← MathLib Explorer

English

If the relation is constantly false, fromRel is empty.

Русский

Если отношение всегда ложно, fromRel пусто.

LaTeX

$$$$ \mathrm{fromRel}(\mathrm{⊥}) = \emptyset. $$$$

Lean4

theorem fromRel_bot : fromRel (fun (_ _ : α) z => z : Symmetric ⊥) = ∅ :=
  by
  apply Set.eq_empty_of_forall_notMem fun e => _
  apply Sym2.ind
  simp [-Set.bot_eq_empty, «Prop».bot_eq_false]

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

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

Разделы

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

Аффилиация

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