biTotal_iff_isEmpty_right — Mathlib

English

Let R be a relation R: α → β → Prop. If α is empty, then BiTotal R is equivalent to β being empty.

Русский

Пусть R — отношение α → β → Prop. Если α пусто, BiTotal(R) эквивалентно пустоте β.

LaTeX

$$$ [\operatorname{IsEmpty}(\alpha)] \Rightarrow \big( \operatorname{BiTotal}(R) \iff \operatorname{IsEmpty}(\beta) \big) $$$

Lean4

theorem biTotal_iff_isEmpty_right [IsEmpty α] : BiTotal R ↔ IsEmpty β := by
  simp only [BiTotal, leftTotal_empty, rightTotal_iff_isEmpty_right, true_and]

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