sup_range_inl_inr — Mathlib

English

The supremum of the ranges of inl and inr is the whole product space M × M₂.

Русский

Наибольший элемент верхнего класса поверхностей образов inl и inr совпадает с полным пространством M × M₂.

LaTeX

$$$ (\\text{range}(\\text{inl } R M M_2)) \\; ⊔ \\; (\\text{range}(\\text{inr } R M M_2)) = ⊤ $$$

Lean4

theorem sup_range_inl_inr : (range <| inl R M M₂) ⊔ (range <| inr R M M₂) = ⊤ :=
  IsCompl.sup_eq_top isCompl_range_inl_inr

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