English
Let R be a relation R: α → β → Prop. If α is empty, then RightTotal R holds if and only if β is empty.
Русский
Пусть R — отношение α → β → Prop. Если α пусто, то RightTotal(R) эквивалентно тому, что β пусто.
LaTeX
$$$ [\operatorname{IsEmpty}(\alpha)] \Rightarrow \big( \operatorname{RightTotal}(R) \iff \operatorname{IsEmpty}(\beta) \big) $$$
Lean4
theorem rightTotal_iff_isEmpty_right [IsEmpty α] : RightTotal R ↔ IsEmpty β := by
simp only [RightTotal, IsEmpty.exists_iff, isEmpty_iff]