Sigma

📁 Source: Mathlib/Data/Set/Sigma.lean

Statistics

Metric	Count
Definitions `sigma`	1
Theorems `sigma`, `sigma_fst`, `sigma_snd`, `biInter_sigma`, `biInter_sigma'`, `biUnion_sigma`, `biUnion_sigma'`, `empty_sigma`, `exists_sigma_iff`, `forall_sigma_iff`, `fst_image_sigma`, `fst_image_sigma_subset`, `image_sigmaMk_preimage_sigmaMap`, `image_sigmaMk_preimage_sigmaMap_subset`, `image_sigmaMk_subset_sigma_left`, `image_sigmaMk_subset_sigma_right`, `image_sigma_eq_iUnion`, `insert_sigma`, `mem_sigma_iff`, `mk_mem_sigma`, `mk_preimage_sigma`, `mk_preimage_sigma_eq_empty`, `mk_preimage_sigma_eq_if`, `mk_preimage_sigma_fn_eq_if`, `mk_sigma_iff`, `preimage_image_sigmaMk_of_ne`, `preimage_sigmaMap_sigma`, `range_sigmaMk`, `sigma_diff_sigma`, `sigma_empty`, `sigma_eq_biUnion`, `sigma_eq_empty_iff`, `sigma_insert`, `sigma_inter_sigma`, `sigma_mono`, `sigma_nonempty_iff`, `sigma_preimage_eq`, `sigma_preimage_left`, `sigma_preimage_right`, `sigma_singleton`, `sigma_subset_iff`, `sigma_subset_preimage_fst`, `sigma_union`, `sigma_univ`, `sigma_univ_range_eq`, `singleton_sigma`, `singleton_sigma_singleton`, `uncurry_preimage_sigma_pi`, `union_sigma`, `univ_sigma_preimage_mk`, `univ_sigma_univ`, `biInf_sigma`, `biInf_sigma'`, `biSup_sigma`, `biSup_sigma'`	55
Total	56

Set

Definitions

Name	Category	Theorems
`sigma` 📖	CompOp	52 math math: `IsCompact.sigma_exists_finite_sigma_eq`, `singleton_sigma_singleton`, `sigma_univ`, `sigma_union`, `mk_preimage_sigma_eq_if`, `sigma_eq_empty_iff`, `sigma_nonempty_iff`, `mk_preimage_sigma_fn_eq_if`, `biInf_sigma`, `insert_sigma`, `sigma_eq_biUnion`, `biSup_sigma'`, `biInter_sigma`, `image_sigmaMk_subset_sigma_left`, `image_sigmaMk_subset_sigma_right`, `mem_sigma_iff`, `Matroid.sigma_ground_eq`, `image_sigma_eq_iUnion`, `sigma_singleton`, `sigma_preimage_eq`, `biUnion_sigma'`, `sigma_univ_range_eq`, `sigma_empty`, `preimage_sigmaMap_sigma`, `biInter_sigma'`, `sigma_preimage_left`, `fst_image_sigma`, `mk_sigma_iff`, `sigma_insert`, `sigma_diff_sigma`, `isCompact_sigma`, `mk_preimage_sigma`, `univ_sigma_preimage_mk`, `exists_sigma_iff`, `biInf_sigma'`, `biSup_sigma`, `sigma_subset_preimage_fst`, `uncurry_preimage_sigma_pi`, `mk_preimage_sigma_eq_empty`, `sigma_preimage_right`, `singleton_sigma`, `union_sigma`, `empty_sigma`, `sigma_inter_sigma`, `fst_image_sigma_subset`, `biUnion_sigma`, `sigma_mono`, `sigma_subset_iff`, `univ_sigma_univ`, `mk_mem_sigma`, `Finset.coe_sigma`, `Nonempty.sigma`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biInter_sigma` 📖	mathematical	—	`iInter` `Set` `instMembership` `sigma`	—	`biInf_sigma`
`biInter_sigma'` 📖	mathematical	—	`iInter` `Set` `instMembership` `sigma`	—	`biInf_sigma'`
`biUnion_sigma` 📖	mathematical	—	`iUnion` `Set` `instMembership` `sigma`	—	`biSup_sigma`
`biUnion_sigma'` 📖	mathematical	—	`iUnion` `Set` `instMembership` `sigma`	—	`biSup_sigma'`
`empty_sigma` 📖	mathematical	—	`sigma` `Set` `instEmptyCollection`	—	—
`exists_sigma_iff` 📖	mathematical	—	`Set` `instMembership` `sigma`	—	—
`forall_sigma_iff` 📖	—	—	—	—	—
`fst_image_sigma` 📖	mathematical	`Nonempty`	`image` `sigma`	—	`HasSubset.Subset.antisymm` `instAntisymmSubset` `fst_image_sigma_subset`
`fst_image_sigma_subset` 📖	mathematical	—	`Set` `instHasSubset` `image` `sigma`	—	`image_subset_iff`
`image_sigmaMk_preimage_sigmaMap` 📖	mathematical	—	`image` `preimage` `Sigma.map`	—	`HasSubset.Subset.antisymm` `instAntisymmSubset` `image_sigmaMk_preimage_sigmaMap_subset`
`image_sigmaMk_preimage_sigmaMap_subset` 📖	mathematical	—	`Set` `instHasSubset` `image` `preimage` `Sigma.map`	—	`image_subset_iff`
`image_sigmaMk_subset_sigma_left` 📖	mathematical	`Set` `instMembership`	`instHasSubset` `image` `sigma`	—	`image_subset_iff`
`image_sigmaMk_subset_sigma_right` 📖	mathematical	`Set` `instMembership`	`instHasSubset` `image` `sigma`	—	`image_subset_iff`
`image_sigma_eq_iUnion` 📖	mathematical	—	`image` `sigma` `iUnion` `Set` `instMembership`	—	`image_congr` `ext`
`insert_sigma` 📖	mathematical	—	`sigma` `Set` `instInsert` `instUnion` `image`	—	—
`mem_sigma_iff` 📖	mathematical	—	`Set` `instMembership` `sigma`	—	—
`mk_mem_sigma` 📖	mathematical	`Set` `instMembership`	`sigma`	—	—
`mk_preimage_sigma` 📖	mathematical	`Set` `instMembership`	`preimage` `sigma`	—	—
`mk_preimage_sigma_eq_empty` 📖	mathematical	`Set` `instMembership`	`preimage` `sigma` `instEmptyCollection`	—	—
`mk_preimage_sigma_eq_if` 📖	mathematical	—	`preimage` `sigma` `Set` `instMembership` `instEmptyCollection`	—	—
`mk_preimage_sigma_fn_eq_if` 📖	mathematical	—	`preimage` `sigma` `Set` `instMembership` `instEmptyCollection`	—	—
`mk_sigma_iff` 📖	mathematical	—	`Set` `instMembership` `sigma`	—	—
`preimage_image_sigmaMk_of_ne` 📖	mathematical	—	`preimage` `image` `Set` `instEmptyCollection`	—	—
`preimage_sigmaMap_sigma` 📖	mathematical	—	`preimage` `Sigma.map` `sigma`	—	—
`range_sigmaMk` 📖	mathematical	—	`range` `preimage` `Set` `instSingletonSet`	—	—
`sigma_diff_sigma` 📖	mathematical	—	`Set` `instSDiff` `sigma` `instUnion` `Pi.sdiff`	—	`ext`
`sigma_empty` 📖	mathematical	—	`sigma` `Set` `instEmptyCollection`	—	—
`sigma_eq_biUnion` 📖	mathematical	—	`sigma` `iUnion` `Set` `instMembership` `image`	—	`ext`
`sigma_eq_empty_iff` 📖	mathematical	—	`sigma` `Set` `instEmptyCollection`	—	`not_nonempty_iff_eq_empty` `Iff.not` `sigma_nonempty_iff`
`sigma_insert` 📖	mathematical	—	`sigma` `Set` `instInsert` `instUnion` `image`	—	—
`sigma_inter_sigma` 📖	mathematical	—	`Set` `instInter` `sigma`	—	—
`sigma_mono` 📖	mathematical	`Set` `instHasSubset`	`sigma`	—	—
`sigma_nonempty_iff` 📖	mathematical	—	`Nonempty` `sigma` `Set` `instMembership`	—	`Nonempty.sigma_snd`
`sigma_preimage_eq` 📖	mathematical	—	`sigma` `preimage`	—	—
`sigma_preimage_left` 📖	mathematical	—	`sigma` `preimage`	—	—
`sigma_preimage_right` 📖	mathematical	—	`sigma` `preimage`	—	—
`sigma_singleton` 📖	mathematical	—	`sigma` `Set` `instSingletonSet` `image`	—	—
`sigma_subset_iff` 📖	mathematical	—	`Set` `instHasSubset` `sigma` `instMembership`	—	—
`sigma_subset_preimage_fst` 📖	mathematical	—	`Set` `instHasSubset` `sigma` `preimage`	—	—
`sigma_union` 📖	mathematical	—	`sigma` `Set` `instUnion`	—	—
`sigma_univ` 📖	mathematical	—	`sigma` `univ` `preimage`	—	—
`sigma_univ_range_eq` 📖	mathematical	—	`sigma` `univ` `range`	—	`ext`
`singleton_sigma` 📖	mathematical	—	`sigma` `Set` `instSingletonSet` `image`	—	—
`singleton_sigma_singleton` 📖	mathematical	—	`sigma` `Set` `instSingletonSet`	—	—
`uncurry_preimage_sigma_pi` 📖	mathematical	—	`preimage` `Sigma.uncurry` `pi` `sigma`	—	`ext`
`union_sigma` 📖	mathematical	—	`sigma` `Set` `instUnion`	—	—
`univ_sigma_preimage_mk` 📖	mathematical	—	`sigma` `univ` `preimage`	—	—
`univ_sigma_univ` 📖	mathematical	—	`sigma` `univ`	—	—

Set.Nonempty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sigma` 📖	mathematical	`Set.Nonempty`	`Set.sigma`	—	—
`sigma_fst` 📖	—	`Set.Nonempty` `Set.sigma`	—	—	—
`sigma_snd` 📖	mathematical	`Set.Nonempty` `Set.sigma`	`Set` `Set.instMembership`	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biInf_sigma` 📖	mathematical	—	`iInf` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf` `Set` `Set.instMembership` `Set.sigma`	—	`biSup_sigma`
`biInf_sigma'` 📖	mathematical	—	`iInf` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf` `Set` `Set.instMembership` `Set.sigma`	—	`biInf_sigma`
`biSup_sigma` 📖	mathematical	—	`iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `Set` `Set.instMembership` `Set.sigma`	—	`eq_of_forall_ge_iff` `iSup_congr_Prop`
`biSup_sigma'` 📖	mathematical	—	`iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `Set` `Set.instMembership` `Set.sigma`	—	`biSup_sigma`

---

← Back to Index