isCompl_range_inl_range_inr — Mathlib

English

The two ranges, range Sum.inl and range Sum.inr, form a partition of the ambient type; they are complementary.

Русский

Два диапазона, range Sum.inl и range Sum.inr, образуют разбиение окружающего типа; они являются комплементами друг друга.

LaTeX

$$$ \\mathrm{IsCompl}(\\mathrm{range}(\\mathrm{Sum.inl}), \\mathrm{range}(\\mathrm{Sum.inr})). $$$

Lean4

theorem isCompl_range_inl_range_inr : IsCompl (range <| @Sum.inl α β) (range Sum.inr) :=
  IsCompl.of_le
    (by
      rintro y ⟨⟨x₁, rfl⟩, ⟨x₂, h⟩⟩
      exact Sum.noConfusion h)
    (by rintro (x | y) - <;> [left; right] <;> exact mem_range_self _)

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