right_subset_compRel

Mathlib.Topology.UniformSpace.Defs

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

English

If idRel ⊆ s, then t ⊆ s ∘ t.

Русский

Если idRel ⊆ s, тогда t ⊆ s ∘ t.

LaTeX

$$$\operatorname{idRel} \subseteq s \Rightarrow t \subseteq s \circ t$$$

Lean4

theorem right_subset_compRel {s t : Set (α × α)} (h : idRel ⊆ s) : t ⊆ s ○ t := fun ⟨x, _y⟩ xy_in =>
  ⟨x, h <| rfl, xy_in⟩

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

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

Разделы

Аффилиация

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