leftTotal_empty — Mathlib

English

Let R be a relation R: α → β → Prop. If α is empty, then LeftTotal R holds (i.e., for every a in α and every b in β there exists a' in α with R a' b).

Русский

Пусть R — отношение R : α → β → Prop. Если α пусто, то выполняется левая полнота LeftTotal(R): для любых a из α и любых b из β существует a' из α, такое что R a' b.

LaTeX

$$$ [\operatorname{IsEmpty}(\alpha)] \Rightarrow \operatorname{LeftTotal}(R) $$$

Lean4

@[simp]
theorem leftTotal_empty [IsEmpty α] : LeftTotal R := by simp only [LeftTotal, IsEmpty.forall_iff]

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