apply_mem_target

Mathlib.Algebra.Group.Action.Equidecomp

URI: https://scilib.ai/kg/mathlib#Equidecomp.apply_mem_target

English

If x belongs to the source of an equidecomposition f, then f(x) belongs to the target of f.

Русский

Если x принадлежит источнику эквидекомпозиции f, то f(x) принадлежит целямf.

LaTeX

$$$\forall f:\mathrm{Equidecomp}(X,G),\; \forall x \in f.source,\; f(x) \in f.target.$$$

Lean4

theorem apply_mem_target {f : Equidecomp X G} {x : X} (h : x ∈ f.source) : f x ∈ f.target := by simp [h]

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

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

Разделы

Аффилиация

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