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 _)