Theorems · Theorem · group theory

Set.singleton_sub

∀ {α : Type u_2} [inst : Sub α] {t : Set α} {a : α}, {a} - t = (fun x1 x2 => x1 - x2) a '' t

Defined in: Mathlib.Algebra.Group.Pointwise.Set.Basic
Cited by: 1 results in Mathlib
Foundations: Depth 8 from the axioms · uses propext, Quot.sound
Assumes: Sub

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
Set.imagestatement · cited by 5,609
Set.substatement · cited by 136
Set.image2_singleton_leftproof · cited by 15

Cited by1

Results whose statement or proof uses this declaration.

SpectrumRestricts.nnreal_iff_spectralRadius_leproof · cited by 1