single_trans_single_of_ne — Mathlib

English

If b1 ≠ b2, then (single a b1).trans (single b2 c) = ⊥.

Русский

Если b1 ≠ b2, то (single a b1).trans (single b2 c) = ⊥.

LaTeX

$$single_trans_single_of_ne \{b_1 b_2 : \beta\} (h : b_1 \neq b_2) (a : \alpha) (c : \gamma) : (single a b_1).trans (single b_2 c) = \\bot$$

Lean4

theorem single_trans_single_of_ne {b₁ b₂ : β} (h : b₁ ≠ b₂) (a : α) (c : γ) : (single a b₁).trans (single b₂ c) = ⊥ :=
  single_trans_of_eq_none _ (single_apply_of_ne h.symm _)

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