cutExpand_singleton

Mathlib.Logic.Hydra

URI: https://scilib.ai/kg/mathlib#Relation.cutExpand_singleton

English

If every element of a finite set s relates to x, then CutExpand r s {x}.

Русский

Если для всех x' ∈ s выполняется r(x', x), то CutExpand r s {x}.

LaTeX

$$$\\forall x' \\in s,\\; r(x',x) \\Rightarrow \\mathrm{CutExpand}(r)(s,\\{x\\})$$$

Lean4

theorem cutExpand_singleton {s x} (h : ∀ x' ∈ s, r x' x) : CutExpand r s { x } :=
  ⟨s, x, h, add_comm s _⟩

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

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

Разделы

Аффилиация

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