compRel_mono

Mathlib.Topology.UniformSpace.Defs

URI: https://scilib.ai/kg/mathlib#compRel_mono

English

If f ⊆ h and g ⊆ k, then f ∘ g ⊆ h ∘ k.

Русский

Если f ⊆ h и g ⊆ k, то f ∘ g ⊆ h ∘ k.

LaTeX

$$$f \circ g \subseteq h \circ k$$$

Lean4

@[mono, gcongr]
theorem compRel_mono {f g h k : Set (α × α)} (h₁ : f ⊆ h) (h₂ : g ⊆ k) : f ○ g ⊆ h ○ k := fun _ ⟨z, h, h'⟩ =>
  ⟨z, h₁ h, h₂ h'⟩

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

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

Разделы

Аффилиация

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