false_of_right_to_left — Mathlib

English

In the join category, there are no arrows from a right object to a left object; any such arrow yields a contradiction (false).

Русский

В соединении категорий не существует стрелок от правого объекта к левому; любая такая стрелка приводит к противоречию (ложь).

LaTeX

$$False$$

Lean4

@[aesop safe destruct (rule_sets := [CategoryTheory])]
theorem false_of_right_to_left {X : D} {Y : C} (f : right X ⟶ left Y) : False :=
  (f : PEmpty).elim

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