Documentation Verification Report

Inclusion

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

Statistics

MetricCount
Definitionsinclusion
1
Theoremscoe_inclusion, eq_of_inclusion_surjective, inclusion_comp_inclusion, inclusion_eq_id, inclusion_inclusion, inclusion_inj, inclusion_injective, inclusion_le_inclusion, inclusion_lt_inclusion, inclusion_mk, inclusion_right, inclusion_self, val_comp_inclusion
13
Total14

Set

Definitions

NameCategoryTheorems
inclusion 📖CompOp
80 mathmath: Affine.Simplex.altitudeFoot_restrict, inclusion_comp_inclusion, Topology.IsClosedEmbedding.inclusion, range_inclusion, inclusion_right, Affine.Simplex.restrict_reindex, Affine.Simplex.faceOppositeCentroid_restrict, Affine.Simplex.restrict_map_restrict, Topology.IsEmbedding.inclusion, val_comp_inclusion, Affine.Simplex.circumradius_restrict, Affine.Simplex.medial_restrict, FirstOrder.Language.Substructure.coe_inclusion, Sublattice.inclusion_apply, Affine.Simplex.ninePointCircle_restrict, Affine.Simplex.face_restrict, Affine.Simplex.interior_restrict, TopologicalSpace.Opens.chartAt_inclusion_symm_eventuallyEq, AffineSubspace.inclusion_linear, Affine.Simplex.altitude_restrict_eq_comap_subtype, FirstOrder.Language.constantsOnMap_inclusion_isExpansionOn, FirstOrder.Language.Term.realize_restrictVarLeft', Affine.Simplex.ExcenterExists.touchpointWeights_restrict, inclusion_eq_id, Order.exists_orderEmbedding_insert, denseRange_inclusion_iff, Affine.Simplex.ExcenterExists.excenter_restrict, Affine.Simplex.map_altitude_restrict, Affine.Simplex.faceOpposite_restrict, MeasurableSet.image_inclusion, Affine.Simplex.exradius_restrict, isUniformEmbedding_set_inclusion, BooleanSubalgebra.coe_inclusion, inclusion_self, iUnionLift_inclusion, Affine.Simplex.circumcenter_restrict, Affine.Simplex.height_restrict, SimpleGraph.induceHomOfLE_apply, Affine.Simplex.incenter_restrict, FirstOrder.Language.BoundedFormula.realize_restrictFreeVar', Affine.Simplex.inradius_restrict, MeasurableSet.image_inclusion', continuous_inclusion, Affine.Simplex.centroid_restrict, Equiv.Set.sumDiffSubset_apply_inr, Affine.Simplex.orthogonalProjectionSpan_restrict, Affine.Simplex.setInterior_restrict, inclusion_inj, Affine.Simplex.excenterWeights_restrict, inclusion_injective, Affine.Simplex.median_restrict, Affine.Simplex.closedInterior_restrict, Affine.Simplex.mongePoint_restrict, Affine.Simplex.eulerPoint_restrict, coe_inclusion, Sublattice.coe_inclusion, AffineSubspace.coe_inclusion_apply, Affine.Simplex.ExcenterExists.touchpoint_restrict, Affine.Simplex.excenterWeightsUnnorm_restrict, OpenPartialHomeomorph.subtypeRestr_symm_eqOn_of_le, IsOpen.isOpenMap_inclusion, Topology.IsOpenEmbedding.inclusion, TopologicalSpace.Opens.isOpenEmbedding_of_le, Equiv.Set.sumDiffSubset_apply_inl, BooleanSubalgebra.inclusion_apply, inclusion_mk, inclusion_le_inclusion, inclusion_inclusion, StructureGroupoid.LocalInvariantProp.liftPropAt_iff_comp_inclusion, inclusion_lt_inclusion, Affine.Simplex.restrict_map_subtype, IsClosed.isClosedMap_inclusion, Affine.Simplex.restrict_map_inclusion, FirstOrder.Language.map_constants_inclusion_isExpansionOn, preimage_iUnionLift, Subrel.coe_inclusionEmbedding, FirstOrder.Language.Term.realize_restrictVar', Affine.Simplex.restrict_points_coe, measurable_inclusion, Affine.Simplex.excenterExists_restrict

Theorems

NameKindAssumesProvesValidatesDepends On
coe_inclusion 📖mathematicalSet
instHasSubset
instMembership
inclusion
eq_of_inclusion_surjective 📖Set
instHasSubset
Elem
inclusion
Subset.antisymm
inclusion_comp_inclusion 📖mathematicalSet
instHasSubset
Elem
inclusion
HasSubset.Subset.trans
instIsTransSubset
HasSubset.Subset.trans
instIsTransSubset
inclusion_inclusion
inclusion_eq_id 📖mathematicalSet
instHasSubset
inclusion
Elem
inclusion_self
inclusion_inclusion 📖mathematicalSet
instHasSubset
inclusion
HasSubset.Subset.trans
instIsTransSubset
HasSubset.Subset.trans
instIsTransSubset
inclusion_inj 📖mathematicalSet
instHasSubset
inclusioninclusion_injective
inclusion_injective 📖mathematicalSet
instHasSubset
Elem
inclusion
inclusion_le_inclusion 📖mathematicalSet
instHasSubset
Elem
instMembership
inclusion
inclusion_lt_inclusion 📖mathematicalSet
instHasSubset
Elem
instMembership
inclusion
inclusion_mk 📖mathematicalSet
instHasSubset
instMembership
inclusion
inclusion_right 📖mathematicalSet
instHasSubset
instMembership
inclusion
inclusion_self 📖mathematicalinclusion
Subset.rfl
Subset.rfl
val_comp_inclusion 📖mathematicalSet
instHasSubset
Elem
instMembership
inclusion

---

← Back to Index