Commit 2023-06-13 06:31 d9d8c53c

View on Github →

feat: port Analysis.Convex.Intrinsic (#4937)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Convex/Intrinsic.lean

added theorem AffineIsometry.image_intrinsicClosure

added theorem AffineIsometry.image_intrinsicFrontier

added theorem AffineIsometry.image_intrinsicInterior

added theorem affineSpan_intrinsicClosure

added theorem closure_diff_intrinsicFrontier

added theorem closure_diff_intrinsicInterior

added theorem interior_subset_intrinsicInterior

added def intrinsicClosure

added theorem intrinsicClosure_diff_intrinsicFrontier

added theorem intrinsicClosure_diff_intrinsicInterior

added theorem intrinsicClosure_empty

added theorem intrinsicClosure_eq_closure

added theorem intrinsicClosure_idem

added theorem intrinsicClosure_mono

added theorem intrinsicClosure_nonempty

added theorem intrinsicClosure_singleton

added theorem intrinsicClosure_subset_affineSpan

added theorem intrinsicClosure_subset_closure

added def intrinsicFrontier

added theorem intrinsicFrontier_empty

added theorem intrinsicFrontier_singleton

added theorem intrinsicFrontier_subset

added theorem intrinsicFrontier_subset_frontier

added theorem intrinsicFrontier_subset_intrinsicClosure

added theorem intrinsicFrontier_union_intrinsicInterior

added def intrinsicInterior

added theorem intrinsicInterior_empty

added theorem intrinsicInterior_nonempty

added theorem intrinsicInterior_singleton

added theorem intrinsicInterior_subset

added theorem intrinsicInterior_union_intrinsicFrontier

added theorem isClosed_intrinsicClosure

added theorem isClosed_intrinsicFrontier

added theorem mem_intrinsicClosure

added theorem mem_intrinsicFrontier

added theorem mem_intrinsicInterior

added theorem subset_intrinsicClosure