disjoint_closure_of_disjoint_support

English

Same as the previous result but stated for sets of permutations within the Equiv.Perm context.

Русский

То же самое утверждение про замыкания над поддержками, но внутри контекста пермутаций эквивалентности.

LaTeX

$$$\\operatorname{Disjoint}(\\overline{S}, \\overline{T}).$$$

Lean4

theorem disjoint_closure_of_disjoint_support {S T : Set (Perm α)}
    (h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support) : _root_.Disjoint (closure S) (closure T) :=
  by
  apply disjoint_of_disjoint_support
  apply disjoint_support_closure_of_disjoint_support
  exact h

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