prodMk_mem_compRel

Mathlib.Topology.UniformSpace.Defs

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

English

If (a,c) ∈ s and (c,b) ∈ t, then (a,b) ∈ s ∘ t.

Русский

Если (a,c) ∈ s и (c,b) ∈ t, то (a,b) ∈ s ∘ t.

LaTeX

$$$(a,c) \in s \land (c,b) \in t \Rightarrow (a,b) \in s \circ t$$$

Lean4

theorem prodMk_mem_compRel {a b c : α} {s t : Set (α × α)} (h₁ : (a, c) ∈ s) (h₂ : (c, b) ∈ t) : (a, b) ∈ s ○ t :=
  ⟨c, h₁, h₂⟩

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

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

Разделы

Аффилиация

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