Theorems · Theorem · group theory

Set.support_subset_subsingleton_of_disjoint_on_support

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Zero β] {s : γ → Set α} (f : α → β),
  Pairwise (Function.onFun Disjoint fun j => s j ∩ Function.support f) →
    ∀ (i : α) (j : γ), i ∈ s j → (Function.support fun d => (s d).indicator f i) ⊆ {j}

Defined in

Mathlib.Algebra.Group.Indicator

Cited by

1 results in Mathlib

Foundations

Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Zero