rightTotal_iff_isEmpty_right — Mathlib

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]

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