biTotal_iff_isEmpty_left — 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}(\beta)] \Rightarrow \big( \operatorname{BiTotal}(R) \iff \operatorname{IsEmpty}(\alpha) \big) $$$

Lean4

theorem biTotal_iff_isEmpty_left [IsEmpty β] : BiTotal R ↔ IsEmpty α := by
  simp only [BiTotal, leftTotal_iff_isEmpty_left, rightTotal_empty, and_true]

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