Image

📁 Source: Mathlib/Data/Set/Lattice/Image.lean

Statistics

Metric	Count
Definitions	0
Theorems `image_biInter_eq`, `image_iInter_eq`, `biInter_image`, `biInter_image2`, `biInter_range`, `biUnion_iInter_of_pairwise_disjoint`, `biUnion_image`, `biUnion_image2`, `biUnion_inter_of_pairwise_disjoint`, `biUnion_preimage_singleton`, `biUnion_prod`, `biUnion_prod'`, `biUnion_range`, `biUnion_range_preimage_singleton`, `bijOn_iInter`, `bijOn_iInter_of_directed`, `bijOn_iUnion`, `bijOn_iUnion_of_directed`, `bijective_iff_bijective_of_iUnion_eq_univ`, `compl_range_subset_kernImage`, `iInter_iInter_eq'`, `iInter_union_iInter`, `iInter₂_union_iInter₂`, `iUnion_iUnion_eq'`, `iUnion_image_left`, `iUnion_image_right`, `iUnion_inter_iUnion`, `iUnion_prod`, `iUnion_prod'`, `iUnion_prod_const`, `iUnion_prod_of_monotone`, `iUnion₂_inter_iUnion₂`, `iUnion₂_prod_const`, `image2_eq_iUnion`, `image2_eq_seq`, `image2_iInter_subset_left`, `image2_iInter_subset_right`, `image2_iInter₂_subset_left`, `image2_iInter₂_subset_right`, `image2_iUnion_left`, `image2_iUnion_right`, `image2_iUnion₂_left`, `image2_iUnion₂_right`, `image2_sInter_left_subset`, `image2_sInter_right_subset`, `image2_sInter_subset_left`, `image2_sInter_subset_right`, `image2_sUnion_left`, `image2_sUnion_right`, `image_eq_iUnion`, `image_iInter`, `image_iInter_subset`, `image_iInter₂`, `image_iInter₂_subset`, `image_iUnion`, `image_iUnion₂`, `image_preimage`, `image_projection_prod`, `image_sInter_subset`, `image_sUnion`, `image_seq`, `inj_on_iUnion_of_directed`, `injective_iff_injective_of_iUnion_eq_univ`, `kernImage_compl`, `kernImage_empty`, `kernImage_eq_compl`, `kernImage_mono`, `kernImage_preimage_eq_iff`, `kernImage_preimage_union`, `kernImage_union_preimage`, `mapsTo_iInter`, `mapsTo_iInter_iInter`, `mapsTo_iInter₂`, `mapsTo_iInter₂_iInter₂`, `mapsTo_iUnion`, `mapsTo_iUnion_iUnion`, `mapsTo_iUnion₂`, `mapsTo_iUnion₂_iUnion₂`, `mapsTo_sInter`, `mapsTo_sUnion`, `monotone_preimage`, `preimage_iInter`, `preimage_iInter₂`, `preimage_iUnion`, `preimage_iUnion₂`, `preimage_kernImage`, `preimage_sInter`, `preimage_sUnion`, `prod_eq_biUnion_left`, `prod_eq_biUnion_right`, `prod_eq_seq`, `prod_iInter`, `prod_iUnion`, `prod_iUnion₂`, `prod_image_seq_comm`, `prod_sInter`, `prod_sUnion`, `range_eq_iUnion`, `sInter_prod`, `sInter_prod_sInter`, `sInter_prod_sInter_subset`, `sUnion_prod_const`, `seq_def`, `seq_mono`, `seq_seq`, `seq_singleton`, `seq_subset`, `singleton_seq`, `surjOn_iInter`, `surjOn_iInter_iInter`, `surjOn_iUnion`, `surjOn_iUnion_iUnion`, `surjOn_iUnion₂`, `surjOn_iUnion₂_iUnion₂`, `surjOn_sUnion`, `surjective_iff_surjective_of_iUnion_eq_univ`, `univ_subtype`	117
Total	117

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biInter_image` 📖	mathematical	—	`iInter` `Set` `instMembership` `image`	—	`iInf_image`
`biInter_image2` 📖	mathematical	—	`iInter` `Set` `instMembership` `image2`	—	`iInf_image2`
`biInter_range` 📖	mathematical	—	`iInter` `Set` `instMembership` `range`	—	`iInf_range`
`biUnion_iInter_of_pairwise_disjoint` 📖	mathematical	`Pairwise` `Function.onFun` `Set` `Disjoint` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`iUnion` `instMembership` `iInter`	—	`biSup_iInter_of_pairwise_disjoint`
`biUnion_image` 📖	mathematical	—	`iUnion` `Set` `instMembership` `image`	—	`iSup_image`
`biUnion_image2` 📖	mathematical	—	`iUnion` `Set` `instMembership` `image2`	—	`iSup_image2`
`biUnion_inter_of_pairwise_disjoint` 📖	mathematical	`Pairwise` `Function.onFun` `Set` `Disjoint` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`iUnion` `instMembership` `instInter`	—	`biSup_inter_of_pairwise_disjoint`
`biUnion_preimage_singleton` 📖	mathematical	—	`iUnion` `Set` `instMembership` `preimage` `instSingletonSet`	—	`preimage_iUnion₂` `biUnion_of_singleton`
`biUnion_prod` 📖	mathematical	—	`iUnion` `Set` `instMembership` `SProd.sprod` `instSProd`	—	`ext` `iUnion_congr_Prop`
`biUnion_prod'` 📖	mathematical	—	`iUnion` `Set` `instMembership` `SProd.sprod` `instSProd`	—	`biSup_prod`
`biUnion_range` 📖	mathematical	—	`iUnion` `Set` `instMembership` `range`	—	`iSup_range`
`biUnion_range_preimage_singleton` 📖	mathematical	—	`iUnion` `Set` `instMembership` `range` `preimage` `instSingletonSet` `univ`	—	`biUnion_preimage_singleton` `preimage_range`
`bijOn_iInter` 📖	mathematical	`BijOn` `InjOn` `iUnion`	`iInter`	—	`mapsTo_iInter_iInter` `BijOn.mapsTo` `InjOn.mono` `iInter_subset` `BijOn.injOn` `surjOn_iInter_iInter` `BijOn.surjOn`
`bijOn_iInter_of_directed` 📖	mathematical	`Directed` `Set` `instHasSubset` `BijOn`	`iInter`	—	`bijOn_iInter` `inj_on_iUnion_of_directed` `BijOn.injOn`
`bijOn_iUnion` 📖	—	`BijOn` `InjOn` `iUnion`	—	—	`mapsTo_iUnion_iUnion` `BijOn.mapsTo` `surjOn_iUnion_iUnion` `BijOn.surjOn`
`bijOn_iUnion_of_directed` 📖	mathematical	`Directed` `Set` `instHasSubset` `BijOn`	`iUnion`	—	`bijOn_iUnion` `inj_on_iUnion_of_directed` `BijOn.injOn`
`bijective_iff_bijective_of_iUnion_eq_univ` 📖	mathematical	`iUnion` `univ`	`Function.Bijective` `Elem` `preimage` `restrictPreimage`	—	`Function.Bijective.eq_1` `injective_iff_injective_of_iUnion_eq_univ` `surjective_iff_surjective_of_iUnion_eq_univ`
`compl_range_subset_kernImage` 📖	mathematical	—	`Set` `instHasSubset` `Compl.compl` `instCompl` `range` `kernImage`	—	`kernImage_empty` `kernImage_mono` `empty_subset`
`iInter_iInter_eq'` 📖	mathematical	—	`iInter`	—	`iInter_congr_Prop` `iInter_exists` `biInter_range`
`iInter_union_iInter` 📖	mathematical	—	`Set` `instUnion` `iInter`	—	`iInter_union` `union_iInter`
`iInter₂_union_iInter₂` 📖	mathematical	—	`Set` `instUnion` `iInter`	—	`iInter_union` `union_iInter`
`iUnion_iUnion_eq'` 📖	mathematical	—	`iUnion`	—	`iUnion_congr_Prop` `iUnion_exists` `biUnion_range`
`iUnion_image_left` 📖	mathematical	—	`iUnion` `Set` `instMembership` `image` `image2`	—	`iUnion_congr_Prop` `image_eq_iUnion` `image2_eq_iUnion`
`iUnion_image_right` 📖	mathematical	—	`iUnion` `Set` `instMembership` `image` `image2`	—	`image2_swap` `iUnion_image_left`
`iUnion_inter_iUnion` 📖	mathematical	—	`Set` `instInter` `iUnion`	—	`iUnion_inter` `inter_iUnion`
`iUnion_prod` 📖	mathematical	—	`iUnion` `SProd.sprod` `Set` `instSProd`	—	`ext`
`iUnion_prod'` 📖	mathematical	—	`iUnion`	—	`iSup_prod`
`iUnion_prod_const` 📖	mathematical	—	`SProd.sprod` `Set` `instSProd` `iUnion`	—	`ext`
`iUnion_prod_of_monotone` 📖	mathematical	`Monotone` `Set` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra`	`iUnion` `SProd.sprod` `instSProd`	—	`ext` `le_sup_left` `le_sup_right`
`iUnion₂_inter_iUnion₂` 📖	mathematical	—	`Set` `instInter` `iUnion`	—	`iUnion_inter` `inter_iUnion`
`iUnion₂_prod_const` 📖	mathematical	—	`SProd.sprod` `Set` `instSProd` `iUnion`	—	`iUnion_prod_const`
`image2_eq_iUnion` 📖	mathematical	—	`image2` `iUnion` `Set` `instMembership` `instSingletonSet`	—	`ext`
`image2_eq_seq` 📖	mathematical	—	`image2` `seq` `image`	—	`seq_eq_image2` `image2_image_left`
`image2_iInter_subset_left` 📖	mathematical	—	`Set` `instHasSubset` `image2` `iInter`	—	`mem_image2_of_mem`
`image2_iInter_subset_right` 📖	mathematical	—	`Set` `instHasSubset` `image2` `iInter`	—	`mem_image2_of_mem`
`image2_iInter₂_subset_left` 📖	mathematical	—	`Set` `instHasSubset` `image2` `iInter`	—	`mem_image2_of_mem`
`image2_iInter₂_subset_right` 📖	mathematical	—	`Set` `instHasSubset` `image2` `iInter`	—	`mem_image2_of_mem`
`image2_iUnion_left` 📖	mathematical	—	`image2` `iUnion`	—	`iUnion_prod_const` `image_iUnion`
`image2_iUnion_right` 📖	mathematical	—	`image2` `iUnion`	—	`prod_iUnion` `image_iUnion`
`image2_iUnion₂_left` 📖	mathematical	—	`image2` `iUnion`	—	`image2_iUnion_left`
`image2_iUnion₂_right` 📖	mathematical	—	`image2` `iUnion`	—	`image2_iUnion_right`
`image2_sInter_left_subset` 📖	mathematical	—	`Set` `instHasSubset` `image2` `sInter` `iInter` `instMembership`	—	—
`image2_sInter_right_subset` 📖	mathematical	—	`Set` `instHasSubset` `image2` `sInter` `iInter` `instMembership`	—	—
`image2_sInter_subset_left` 📖	mathematical	—	`Set` `instHasSubset` `image2` `sInter` `iInter` `instMembership`	—	`sInter_eq_biInter` `image2_iInter₂_subset_left`
`image2_sInter_subset_right` 📖	mathematical	—	`Set` `instHasSubset` `image2` `sInter` `iInter` `instMembership`	—	`sInter_eq_biInter` `image2_iInter₂_subset_right`
`image2_sUnion_left` 📖	mathematical	—	`image2` `sUnion` `iUnion` `Set` `instMembership`	—	`ext`
`image2_sUnion_right` 📖	mathematical	—	`image2` `sUnion` `iUnion` `Set` `instMembership`	—	`ext`
`image_eq_iUnion` 📖	mathematical	—	`image` `iUnion` `Set` `instMembership` `instSingletonSet`	—	`ext`
`image_iInter` 📖	mathematical	`Function.Bijective`	`image` `iInter`	—	`isEmpty_or_nonempty` `iInter_of_empty` `image_univ_of_surjective` `Function.Bijective.surjective` `InjOn.image_iInter_eq` `Function.Injective.injOn` `Function.Bijective.injective`
`image_iInter_subset` 📖	mathematical	—	`Set` `instHasSubset` `image` `iInter`	—	`MapsTo.image_subset` `mapsTo_iInter_iInter` `mapsTo_image`
`image_iInter₂` 📖	mathematical	`Function.Bijective`	`image` `iInter`	—	`image_iInter`
`image_iInter₂_subset` 📖	mathematical	—	`Set` `instHasSubset` `image` `iInter`	—	`MapsTo.image_subset` `mapsTo_iInter₂_iInter₂` `mapsTo_image`
`image_iUnion` 📖	mathematical	—	`image` `iUnion`	—	`ext` `exists_swap`
`image_iUnion₂` 📖	mathematical	—	`image` `iUnion`	—	`image_iUnion`
`image_preimage` 📖	mathematical	—	`GaloisConnection` `Set` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra` `image` `preimage`	—	`image_subset_iff`
`image_projection_prod` 📖	mathematical	`Nonempty` `pi` `univ`	`image` `iInter` `preimage`	—	`Subset.antisymm` `Function.forall_update_iff` `Function.update_self`
`image_sInter_subset` 📖	mathematical	—	`Set` `instHasSubset` `image` `sInter` `iInter` `instMembership`	—	`sInter_eq_biInter` `image_iInter₂_subset`
`image_sUnion` 📖	mathematical	—	`image` `sUnion` `Set`	—	`ext` `sUnion_image`
`image_seq` 📖	mathematical	—	`image` `seq`	—	`image_image2` `image2_image_left` `image2_congr`
`inj_on_iUnion_of_directed` 📖	mathematical	`Directed` `Set` `instHasSubset` `InjOn`	`iUnion`	—	`mem_iUnion`
`injective_iff_injective_of_iUnion_eq_univ` 📖	mathematical	`iUnion` `univ`	`Elem` `preimage` `restrictPreimage`	—	`restrictPreimage_injective` `mem_iUnion`
`kernImage_compl` 📖	mathematical	—	`kernImage` `Compl.compl` `Set` `instCompl` `image`	—	`kernImage_eq_compl` `compl_compl`
`kernImage_empty` 📖	mathematical	—	`kernImage` `Set` `instEmptyCollection` `Compl.compl` `instCompl` `range`	—	`kernImage_eq_compl` `compl_empty` `image_univ`
`kernImage_eq_compl` 📖	mathematical	—	`kernImage` `Compl.compl` `Set` `instCompl` `image`	—	`GaloisConnection.u_unique` `preimage_kernImage` `GaloisConnection.compl` `image_preimage` `preimage_compl` `compl_compl`
`kernImage_mono` 📖	mathematical	—	`Monotone` `Set` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra` `kernImage`	—	`GaloisConnection.monotone_u` `preimage_kernImage`
`kernImage_preimage_eq_iff` 📖	mathematical	—	`kernImage` `preimage` `Set` `instHasSubset` `Compl.compl` `instCompl` `range`	—	`kernImage_eq_compl` `preimage_compl` `compl_eq_comm` `image_preimage_eq_iff` `compl_subset_comm`
`kernImage_preimage_union` 📖	mathematical	—	`kernImage` `Set` `instUnion` `preimage`	—	`union_comm` `kernImage_union_preimage`
`kernImage_union_preimage` 📖	mathematical	—	`kernImage` `Set` `instUnion` `preimage`	—	`kernImage_eq_compl` `compl_union` `preimage_compl` `image_inter_preimage` `compl_inter` `compl_compl`
`mapsTo_iInter` 📖	mathematical	—	`MapsTo` `iInter`	—	`mapsTo_sInter` `forall_mem_range`
`mapsTo_iInter_iInter` 📖	mathematical	`MapsTo`	`iInter`	—	`mapsTo_iInter` `MapsTo.mono_left` `iInter_subset`
`mapsTo_iInter₂` 📖	mathematical	—	`MapsTo` `iInter`	—	—
`mapsTo_iInter₂_iInter₂` 📖	mathematical	`MapsTo`	`iInter`	—	`mapsTo_iInter_iInter`
`mapsTo_iUnion` 📖	mathematical	—	`MapsTo` `iUnion`	—	`iUnion_subset_iff`
`mapsTo_iUnion_iUnion` 📖	mathematical	`MapsTo`	`iUnion`	—	`mapsTo_iUnion` `MapsTo.mono_right` `subset_iUnion`
`mapsTo_iUnion₂` 📖	mathematical	—	`MapsTo` `iUnion`	—	`iUnion₂_subset_iff`
`mapsTo_iUnion₂_iUnion₂` 📖	mathematical	`MapsTo`	`iUnion`	—	`mapsTo_iUnion_iUnion`
`mapsTo_sInter` 📖	mathematical	—	`MapsTo` `sInter`	—	`forall₂_swap`
`mapsTo_sUnion` 📖	mathematical	—	`MapsTo` `sUnion`	—	`sUnion_subset_iff`
`monotone_preimage` 📖	mathematical	—	`Monotone` `Set` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra` `preimage`	—	`preimage_mono`
`preimage_iInter` 📖	mathematical	—	`preimage` `iInter`	—	`ext`
`preimage_iInter₂` 📖	mathematical	—	`preimage` `iInter`	—	`preimage_iInter`
`preimage_iUnion` 📖	mathematical	—	`preimage` `iUnion`	—	`ext`
`preimage_iUnion₂` 📖	mathematical	—	`preimage` `iUnion`	—	`preimage_iUnion`
`preimage_kernImage` 📖	mathematical	—	`GaloisConnection` `Set` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra` `preimage` `kernImage`	—	`subset_kernImage_iff`
`preimage_sInter` 📖	mathematical	—	`preimage` `sInter` `iInter` `Set` `instMembership`	—	`sInter_eq_biInter` `preimage_iInter₂`
`preimage_sUnion` 📖	mathematical	—	`preimage` `sUnion` `iUnion` `Set` `instMembership`	—	`sUnion_eq_biUnion` `preimage_iUnion₂`
`prod_eq_biUnion_left` 📖	mathematical	—	`SProd.sprod` `Set` `instSProd` `iUnion` `instMembership` `image`	—	`iUnion_image_left` `image2_mk_eq_prod`
`prod_eq_biUnion_right` 📖	mathematical	—	`SProd.sprod` `Set` `instSProd` `iUnion` `instMembership` `image`	—	`iUnion_image_right` `image2_mk_eq_prod`
`prod_eq_seq` 📖	mathematical	—	`SProd.sprod` `Set` `instSProd` `seq` `image`	—	`seq_eq_image2` `image2_image_left` `image2_mk_eq_prod`
`prod_iInter` 📖	mathematical	—	`SProd.sprod` `Set` `instSProd` `iInter`	—	`ext`
`prod_iUnion` 📖	mathematical	—	`SProd.sprod` `Set` `instSProd` `iUnion`	—	`ext`
`prod_iUnion₂` 📖	mathematical	—	`SProd.sprod` `Set` `instSProd` `iUnion`	—	`prod_iUnion`
`prod_image_seq_comm` 📖	mathematical	—	`seq` `image`	—	`prod_eq_seq` `image_swap_prod` `image_seq` `image_comp`
`prod_sInter` 📖	mathematical	`Nonempty` `Set`	`SProd.sprod` `instSProd` `sInter` `iInter` `instMembership`	—	`sInter_singleton` `sInter_prod_sInter` `singleton_nonempty` `iInter_congr_Prop` `singleton_prod` `iInter_exists` `biInter_and'` `iInter_iInter_eq_right`
`prod_sUnion` 📖	mathematical	—	`SProd.sprod` `Set` `instSProd` `sUnion` `image`	—	`sUnion_eq_biUnion` `biUnion_image` `prod_iUnion₂`
`range_eq_iUnion` 📖	mathematical	—	`range` `iUnion` `Set` `instSingletonSet`	—	`ext`
`sInter_prod` 📖	mathematical	`Nonempty` `Set`	`SProd.sprod` `instSProd` `sInter` `iInter` `instMembership`	—	`sInter_singleton` `sInter_prod_sInter` `singleton_nonempty` `iInter_congr_Prop` `prod_singleton` `iInter_exists` `biInter_and'` `iInter_iInter_eq_right`
`sInter_prod_sInter` 📖	mathematical	`Nonempty` `Set`	`SProd.sprod` `instSProd` `sInter` `iInter` `instMembership`	—	`Subset.antisymm` `sInter_prod_sInter_subset` `mem_iInter₂`
`sInter_prod_sInter_subset` 📖	mathematical	—	`Set` `instHasSubset` `SProd.sprod` `instSProd` `sInter` `iInter` `instMembership`	—	`subset_iInter₂`
`sUnion_prod_const` 📖	mathematical	—	`SProd.sprod` `Set` `instSProd` `sUnion` `image`	—	`sUnion_eq_biUnion` `iUnion₂_prod_const` `biUnion_image`
`seq_def` 📖	mathematical	—	`seq` `iUnion` `Set` `instMembership` `image`	—	`seq_eq_image2` `iUnion_image_left`
`seq_mono` 📖	mathematical	`Set` `instHasSubset`	`seq`	—	`image2_subset`
`seq_seq` 📖	mathematical	—	`seq` `image`	—	`image2_image_left` `image2_congr` `image2_assoc`
`seq_singleton` 📖	mathematical	—	`seq` `Set` `instSingletonSet` `image`	—	`image2_singleton_right`
`seq_subset` 📖	mathematical	—	`Set` `instHasSubset` `seq` `instMembership`	—	`image2_subset_iff`
`singleton_seq` 📖	mathematical	—	`seq` `Set` `instSingletonSet` `image`	—	`image2_singleton_left`
`surjOn_iInter` 📖	mathematical	`SurjOn` `InjOn` `iUnion`	`iInter`	—	`InjOn.image_iInter_eq` `mem_iInter`
`surjOn_iInter_iInter` 📖	mathematical	`SurjOn` `InjOn` `iUnion`	`iInter`	—	`surjOn_iInter` `SurjOn.mono` `Subset.refl` `iInter_subset`
`surjOn_iUnion` 📖	mathematical	`SurjOn`	`iUnion`	—	`surjOn_sUnion` `forall_mem_range`
`surjOn_iUnion_iUnion` 📖	mathematical	`SurjOn`	`iUnion`	—	`surjOn_iUnion` `SurjOn.mono` `subset_iUnion` `Subset.refl`
`surjOn_iUnion₂` 📖	mathematical	`SurjOn`	`iUnion`	—	`surjOn_iUnion`
`surjOn_iUnion₂_iUnion₂` 📖	mathematical	`SurjOn`	`iUnion`	—	`surjOn_iUnion_iUnion`
`surjOn_sUnion` 📖	mathematical	`SurjOn`	`sUnion`	—	—
`surjective_iff_surjective_of_iUnion_eq_univ` 📖	mathematical	`iUnion` `univ`	`Elem` `preimage` `restrictPreimage`	—	`restrictPreimage_surjective` `mem_iUnion`
`univ_subtype` 📖	mathematical	—	`univ` `iUnion` `Set` `instSingletonSet`	—	`ext`

Set.InjOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image_biInter_eq` 📖	mathematical	`Set.InjOn` `Set.iUnion`	`Set.image` `Set.iInter`	—	`iInf_subtype'` `image_iInter_eq` `nonempty_subtype` `iSup_subtype'`
`image_iInter_eq` 📖	mathematical	`Set.InjOn` `Set.iUnion`	`Set.image` `Set.iInter`	—	`Set.Subset.antisymm` `Set.image_iInter_subset` `Set.mem_iInter` `Set.subset_iUnion`

---

← Back to Index