mem_cycleFactorsFinset_support_le

English

Every cycle factor of f has its support contained in the support of f.

Русский

Опора каждого факторного цикла f подмножество опоры f.

LaTeX

$$$\forall p \in cycleFactorsFinset(f),\; p.support \subseteq f.support$$$

Lean4

theorem mem_cycleFactorsFinset_support_le {p f : Perm α} (h : p ∈ cycleFactorsFinset f) : p.support ≤ f.support :=
  by
  rw [mem_cycleFactorsFinset_iff] at h
  intro x hx
  rwa [mem_support, ← h.right x hx, ← mem_support]

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