biTotal_empty — Mathlib

English

Let R be a relation R: α → β → Prop. If α is empty and β is empty, then BiTotal R holds.

Русский

Пусть R — отношение α → β → Prop. Если оба домена пусты, то BiTotal(R) выполняется.

LaTeX

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

Lean4

@[simp]
theorem biTotal_empty [IsEmpty α] [IsEmpty β] : BiTotal R :=
  ⟨leftTotal_empty R, rightTotal_empty R⟩

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