rightTotal_empty

Mathlib.Logic.IsEmpty

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

English

Let R be a relation R: α → β → Prop. If β is empty, then RightTotal R holds.

Русский

Пусть R — отношение α → β → Prop. Если β пусто, то RightTotal(R) выполняется.

LaTeX

$$$ [\operatorname{IsEmpty}(\beta)] \Rightarrow \operatorname{RightTotal}(R) $$$

Lean4

@[simp]
theorem rightTotal_empty [IsEmpty β] : RightTotal R := by simp only [RightTotal, IsEmpty.forall_iff]

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

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

Разделы

Аффилиация

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