equivalence_join_red — Mathlib

English

If Red L1 L2 and Red L2 L1, then L1 = L2.

Русский

Если Red L1 L2 и Red L2 L1, то L1 = L2.

LaTeX

$$$Red(L_1,L_2) \land Red(L_2,L_1) \Rightarrow L_1 = L_2$$$

Lean4

@[to_additive]
theorem equivalence_join_red : Equivalence (Join (@Red α)) :=
  equivalence_join_reflTransGen fun _ b c hab hac =>
    match b, c, Red.Step.diamond hab hac rfl with
    | b, _, Or.inl rfl => ⟨b, by rfl, by rfl⟩
    | _, _, Or.inr ⟨d, hbd, hcd⟩ => ⟨d, ReflGen.single hbd, ReflTransGen.single hcd⟩

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