Mathlib Map

Theorems · Theorem · group theory

Set.neg_subset_neg

∀ {α : Type u_2} [inst : InvolutiveNeg α] {s t : Set α}, -s ⊆ -t ↔ s ⊆ t
Defined in
Mathlib.Algebra.Group.Pointwise.Set.Basic
Cited by
5 results in Mathlib
Foundations
Depth 26 from the axioms · uses propext, Quot.sound
Assumes
InvolutiveNeg
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set.neg_subset · cited by 6Set.neg_subsetBalanced.neg · cited by 2Balanced.negMeasureTheory.hasFDerivAt_convolution_right_with_param · cited by 1MeasureTheory.hasFDerivAt…Submodule.neg_le_neg · cited by 0Submodule.neg_le_negAddSubmonoid.neg_le_neg · cited by 0AddSubmonoid.neg_le_negSet · cited by 53352SetEquiv.surjective · cited by 198Equiv.surjectiveSet.neg · cited by 168Set.negInvolutiveNeg · cited by 151InvolutiveNegEquiv.neg · cited by 53Equiv.negFunction.Surjective.preimage_subset_preimage_iff · cited by 6Surjective.preimage_subse…Set.neg_subset_negCITED BYCITES

Cites6

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

Cited by5

Results whose statement or proof uses this declaration.