mem_imp

Mathlib.GroupTheory.Perm.Support

URI: https://scilib.ai/kg/mathlib#Equiv.Perm.Disjoint.mem_imp

English

If f and g are disjoint, then any element of supp(f) is not in supp(g).

Русский

Если f и g дисjoint, то элемент опоры f не принадлежит опоре g.

LaTeX

$$$f.\operatorname{Disjoint} g \Rightarrow \forall x, x \in \operatorname{supp}(f) \Rightarrow x \notin \operatorname{supp}(g).$$$

Lean4

theorem mem_imp (h : Disjoint f g) {x : α} (hx : x ∈ f.support) : x ∉ g.support :=
  disjoint_left.mp h.disjoint_support hx

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

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

Разделы

Аффилиация

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