Documentation Verification Report

SurjOn

📁 Source: Mathlib/Order/Interval/Set/SurjOn.lean

Statistics

Metric	Count
Definitions `SurjOn`	1
Theorems `surjOn_Icc_of_monotone_surjective`, `surjOn_Ici_of_monotone_surjective`, `surjOn_Ico_of_monotone_surjective`, `surjOn_Iic_of_monotone_surjective`, `surjOn_Iio_of_monotone_surjective`, `surjOn_Ioc_of_monotone_surjective`, `surjOn_Ioi_of_monotone_surjective`, `surjOn_Ioo_of_monotone_surjective`	8
Total	9

Set

Definitions

Name	Category	Theorems
`SurjOn` 📖	MathDef	108 math math: `SurjOn.union_union`, `SurjOn.comp_right`, `LinearMap.injOn_iff_surjOn`, `surjOn_image`, `surjOn_iUnion`, `SimpleGraph.TripartiteFromTriangles.toTriangle_surjOn`, `ApproximatesLinearOn.surjOn_closedBall_of_nonlinearRightInverse`, `surjOn_iff_surjective`, `surjOn_univ_of_subsingleton_nonempty`, `surjOn_iInter_iInter`, `ModularGroup.bottom_row_surj`, `SurjOn.mono`, `ax_grothendieck_of_definable`, `Function.Semiconj.surjOn_image`, `Real.surjOn_log'`, `surjOn_empty`, `Real.cosh_surjOn`, `surjOn_iUnion₂_iUnion₂`, `Finset.image_surjOn_powerset`, `projIic_surjOn`, `Subgroup.leftCoset_cover_const_iff_surjOn`, `surjOn_Ioo_of_monotone_surjective`, `Real.surjOn_logb'`, `surjOn_iInter`, `Real.artanh_surjOn`, `surjOn_univ`, `Real.ofDigits_SurjOn`, `ContinuousOn.surjOn_uIcc`, `Finset.intervalGapsWithin_surjOn`, `SurjOn.inter_inter`, `SurjOn.of_comp`, `surjOn_of_subsingleton'`, `surjOn_sUnion`, `surjOn_of_subsingleton`, `EqOn.surjOn_iff`, `ContinuousOn.surjOn_of_tendsto'`, `surjOn_comp_iff`, `surjOn_empty_iff`, `SurjOn.iterate`, `ContinuousOn.surjOn_of_tendsto`, `Function.Surjective.surjOn`, `SurjOn.extendDomain`, `Filter.map_surjOn_Iic_iff_surjOn`, `Finset.sup_preimage_self`, `surjOn_iff_exists_bijOn_subset`, `OpenPartialHomeomorph.surjOn`, `AddSubgroup.leftCoset_cover_const_iff_surjOn`, `BijOn.surjOn`, `NormedAddGroupHom.SurjectiveOnWith.surjOn`, `Ordinal.typein_surjOn`, `Real.surjOn_log`, `RightInvOn.surjOn`, `AddSubmonoid.surjOn_iff_le_map`, `Real.surjOn_sin`, `surjOn_id`, `SurjOn.inter`, `SurjOn.filter_map_Iic`, `List.toFinset_surj_on`, `surjOn_Ioc_of_monotone_surjective`, `SurjOn.congr`, `ContinuousOn.surjOn_Icc`, `SurjOn.prodMap`, `Filter.map_surjOn_Iic_iff_le_map`, `Real.surjOn_cos`, `Finset.surjOn_of_injOn_of_card_le`, `surjOn_Iio_of_monotone_surjective`, `SurjOn.comp`, `Real.surjOn_logb`, `Circle.surjOn_exp_neg_pi_pi`, `PrincipalSeg.surjOn`, `FirstOrder.realize_genericPolyMapSurjOnOfInjOn`, `surjective_iff_surjOn_univ`, `surjOn_Ioi_of_monotone_surjective`, `Finite.surjOn_iff_bijOn_of_mapsTo`, `surjOn_extremePoints_image`, `SimpleGraph.Copy.toSubgraph_surjOn`, `projIci_surjOn`, `SurjOn.perm_pow`, `SimpleGraph.Coloring.surjOn_of_card_le_isClique`, `surjOn_Icc_of_monotone_surjective`, `AddSubgroup.surjOn_iff_le_map`, `surjOn_iff_exists_map_subtype`, `projIcc_surjOn`, `ax_grothendieck_of_locally_finite`, `MapsTo.surjOn_compl`, `Function.Semiconj.surjOn_range`, `surjOn_iUnion_iUnion`, `LeftInvOn.surjOn`, `Bundle.Trivialization.proj_surjOn_baseSet`, `surjOn_Ico_of_monotone_surjective`, `surjOn_singleton`, `Real.arcosh_surjOn`, `Submonoid.surjOn_iff_le_map`, `Real.surjOn_tan`, `surjOn_Ici_of_monotone_surjective`, `PartialEquiv.surjOn`, `Subgroup.surjOn_iff_le_map`, `Bundle.Pretrivialization.proj_surjOn_baseSet`, `surjOn_Iic_of_monotone_surjective`, `Real.tanh_surjOn`, `ax_grothendieck_zeroLocus`, `MapsTo.restrict_surjective_iff`, `SurjOn.comp_left`, `Finpartition.part_surjOn`, `Submodule.surjOn_iff_le_map`, `surjOn_iUnion₂`, `SurjOn.union`, `image_eq_iff_surjOn_mapsTo`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`surjOn_Icc_of_monotone_surjective` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE`	`Set.SurjOn` `Set.Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Set.eq_endpoints_or_mem_Ioo_of_mem_Icc` `Set.left_mem_Icc` `Set.right_mem_Icc` `Set.image_mono` `Set.Ioo_subset_Icc_self` `surjOn_Ioo_of_monotone_surjective`
`surjOn_Ici_of_monotone_surjective` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set.SurjOn` `Set.Ici` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Set.Ioi_union_left` `Set.SurjOn.union_union` `surjOn_Ioi_of_monotone_surjective` `Set.surjOn_image` `Set.image_singleton`
`surjOn_Ico_of_monotone_surjective` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set.SurjOn` `Set.Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`lt_or_ge` `Set.eq_left_or_mem_Ioo_of_mem_Ico` `Set.mem_image_of_mem` `Set.left_mem_Ico` `Set.image_mono` `Set.Ioo_subset_Ico_self` `surjOn_Ioo_of_monotone_surjective` `Set.Ico_eq_empty` `LE.le.not_gt` `Set.surjOn_empty`
`surjOn_Iic_of_monotone_surjective` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set.SurjOn` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`surjOn_Ici_of_monotone_surjective` `Monotone.dual`
`surjOn_Iio_of_monotone_surjective` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set.SurjOn` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`surjOn_Ioi_of_monotone_surjective` `Monotone.dual`
`surjOn_Ioc_of_monotone_surjective` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set.SurjOn` `Set.Ioc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Set.Ico_toDual` `surjOn_Ico_of_monotone_surjective` `Monotone.dual`
`surjOn_Ioi_of_monotone_surjective` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set.SurjOn` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Set.compl_Iic` `compl_compl` `Set.MapsTo.surjOn_compl` `LE.le.not_gt`
`surjOn_Ioo_of_monotone_surjective` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set.SurjOn` `Set.Ioo` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Set.mem_Ioo` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_and_eq` `LT.lt.not_ge` `Monotone.reflect_lt`

---

← Back to Index