English
The ranges of the left and right inclusion maps are complementary in M × M₂: range(inl) ⊔ range(inr) = ⊤ and their intersection is {0}.
Русский
Образы левого и правого включения в произведение образуют дополнение; их сумма равна ⊤ и их пересечение тривиально.
LaTeX
$$$ IsCompl(\\text{range}(\\text{inl } R M M_2)) \\; (\\text{range}(\\text{inr } R M M_2)) $$$
Lean4
theorem isCompl_range_inl_inr : IsCompl (range <| inl R M M₂) (range <| inr R M M₂) :=
by
constructor
· rw [disjoint_def]
rintro ⟨_, _⟩ ⟨x, hx⟩ ⟨y, hy⟩
simp only [Prod.ext_iff, inl_apply, inr_apply] at hx hy ⊢
exact ⟨hy.1.symm, hx.2.symm⟩
· rw [codisjoint_iff_le_sup]
rintro ⟨x, y⟩ -
simp only [mem_sup, mem_range]
refine ⟨(x, 0), ⟨x, rfl⟩, (0, y), ⟨y, rfl⟩, ?_⟩
simp
