embeddingUpInt_areComplementary — Mathlib

English

If n0 and n1 are integers with n0 + 1 = n1, then the two canonical embeddings embeddingUpIntLE n0 and embeddingUpIntGE n1 are complementary, i.e., their boundary data are disjoint and cover the ambient index set.

Русский

Если целые числа n0, n1 удовлетворяют n0 + 1 = n1, то канонические вложения embeddingUpIntLE n0 и embeddingUpIntGE n1 являются комплементарными: их границы не пересекаются и пополняют индексное множество.

LaTeX

$$$AreComplementary( embeddingUpIntLE\\, n_0,\; embeddingUpIntGE\\, n_1)\\; (\\text{при } n_0+1=n_1)$$$

Lean4

theorem embeddingUpInt_areComplementary (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) :
    AreComplementary (embeddingUpIntLE n₀) (embeddingUpIntGE n₁)
    where
  disjoint i₁ i₂ := by dsimp; omega
  union
    i := by
    by_cases hi : i ≤ n₀
    · obtain ⟨k, rfl⟩ := Int.exists_add_of_le hi
      exact Or.inl ⟨k, by dsimp; omega⟩
    · obtain ⟨k, rfl⟩ := Int.exists_add_of_le (show n₁ ≤ i by omega)
      exact Or.inr ⟨k, rfl⟩

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