cod_mono

Mathlib.Data.Rel

URI: https://scilib.ai/kg/mathlib#SetRel.cod_mono

English

If R1 ⊆ R2, then cod(R1) ⊆ cod(R2).

Русский

Если R1 ⊆ R2, то cod(R1) ⊆ cod(R2).

LaTeX

$$R_1 \subseteq R_2 \Rightarrow \operatorname{cod}(R_1) \subseteq \operatorname{cod}(R_2)$$

Lean4

@[gcongr]
theorem cod_mono (h : R₁ ≤ R₂) : R₁.cod ⊆ R₂.cod := fun _b ⟨a, hab⟩ ↦ ⟨a, h hab⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru