leftTotal_iff_isEmpty_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem leftTotal_iff_isEmpty_left [IsEmpty β] : LeftTotal R ↔ IsEmpty α := by
  simp only [LeftTotal, IsEmpty.exists_iff, isEmpty_iff]

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