symm — Mathlib

English

If e1 and e2 are complementary embeddings into a common complex shape, then reversing their order yields AreComplementary e2 e1.

Русский

Если существует взаимодополнение встраиваний e1 и e2 в общую форму, то перестановка ими мест друг относительно друга сохраняет свойство взаимодополнения.

LaTeX

$$AreComplementary e1 e2 → AreComplementary e2 e1$$

Lean4

theorem symm : AreComplementary e₂ e₁
    where
  disjoint i₂ i₁ := (ac.disjoint i₁ i₂).symm
  union i := (ac.union i).symm

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