feat (Topology/Compactness/CompactSystem): Closed and compact square cylinders form a compact system.#25904
Closed
pfaffelh wants to merge 228 commits intoleanprover-community:masterfrom
Closed
feat (Topology/Compactness/CompactSystem): Closed and compact square cylinders form a compact system.#25904pfaffelh wants to merge 228 commits intoleanprover-community:masterfrom
pfaffelh wants to merge 228 commits intoleanprover-community:masterfrom
Conversation
…ContinuousLinearEquiv` (leanprover-community#25809) This is needed before we can switch the definition of models with corners in leanprover-community#23658, as general diffeomorphisms don't send convex sets to convex sets.
The docstring of `IsLocalHom` talked about ring morphism in a context of a map of monoids.
…ommunity#25810) We update `README.md` to reflect the new contribution process. Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>
…anprover-community#25695) The impetus for these lemmas was proving the triangle inequality for the metric structure on `α →ᵤ β`, where `edist f g := ⨆ x, edist (f x) (g x)`, which takes place in leanprover-community#25632. This PR continues the work from leanprover-community#25633. Original PR: leanprover-community#25633
These will just cause periodic errors if the forked repo has actions enabled.
…rover-community#25793) The GitHub action we use to determine PR metadata (used to change labels and take actions based on existing labels) does not work for PRs from forks. If it is a PR from a fork, then the workflow context already contains the required data. I could not find an action that has the required functionality and supports both forks and non-fork pushes. So we write a little bit of code to select the right data source. Test PR: leanprover-community#25807.
…er-community#25764) ... and remove two `erw`s on the way.
This is used to define the fpqc topology for schemes.
….lean` to `ClearExclamation.lean`) (leanprover-community#25820) Some context: * filename Clear!.lean contains illegal character "!" (leanprover-community#1212) * chore(Mathlib/Tactic/Clear!): rename `Clear!.lean` to `ClearExclamation.lean` to avoid the illegal character `!` (leanprover-community#12757) This PR renames `MathlibTest/Clear!.lean` to `MathlibTest/ClearExclamation.lean` to avoid shell quoting issues caused by the `!` character in file names. For example: ``` % ls -l MathlibTest/Clear!.lean zsh: event not found: .lean % ls -l "MathlibTest/Clear!.lean" zsh: event not found: .lean ``` See issue leanprover-community#1212 for some additional context.
…y#25350) This PR adds the simple autoparam `by intro; first | rfl | ext <;> rfl` for the fields `left_inv`, `right_inv` of `Equiv`, and removes explicit terms in favor of the autoparam across mathlib in many (but possibly not all) applicable cases. It also adds the same autoparam to the corresponding fields of `LieEquiv` for parity (which is used nontrivially in `LieSubalgebra.topEquiv` in `Mathlib.Algebra.Lie.Submodule`).
…eanprover-community#25696) Often the natural isomorphism will be defined such that the components are eqToHom's, hence I suggest that a default proof is given by `by aesop_cat`.
…isoWhisker (leanprover-community#25745) Using the extension of `reassoc` to equality of isomorphisms, tags some lemmas in `CategoryTheory.Whiskering` with this new version of the attribute. Co-authored-by: Kyle Miller <kmill31415@gmail.com>
…y#25062) Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
… bifunctors (leanprover-community#25733) Introduce a typeclass `PreservesColimit₂` that bundles the assumption that a bifunctor preserves a pair of colimit diagrams in each of its variables. This is stated in terms of a construction `Functor.mapCocone₂` that applies a bifunctor `G` to a pair of cocones to get a cocone over the uncurryfication of `whiskeringLeft₂ _|>.obj _|>.obj _|>.obj G`. The cocone points of this construction is definitionally the evaluation of `G` at the cocone points of the two cocones given as parameters. We give helper functions to extract isomorphisms with abstract colimits out of this typeclass, and we characterize these isomorphisms with respect to the canonical maps to the colimits. The dual typeclass for limits is also introduced.
leanprover-community#15420) This is a partial attempt at leanprover-community#15410, porting [leanprover-community#8009](leanprover-community/mathlib3#8009) Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…eton (leanprover-community#25839) Co-authored-by: Christian Merten <136261474+chrisflav@users.noreply.github.com>
…eanprover-community#25773) This PR rearranges the `gcongr` attributes so that `gcongr` and `grewrite` have minimal imports. This means that it can be imported in `Mathlib.Tactic.Common`. There was also an unused import in Tactic.Hint that I removed `positivity` now gets tagged as the discharger for `gcongr` immediately, which makes some proofs shorter. `Nat.succ_le_succ` was tagged twice with `gcongr`, so I removed the loose tag.
…y#24796) Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
…ds is nonempty (leanprover-community#25105) Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
…community#25815) Extra lemmas about group cohomology in preparation for leanprover-community#25310.
The following example shows test cases that `hint` now supports, which were unsupported prior to this PR: ``` import Mathlib -- The tactics registered in this PR register_hint compute_degree register_hint field_simp register_hint finiteness -- "hint" now correctly suggests "compute_degree" which closes the goal (no closing tactic suggested prior to this PR) open Polynomial in example : natDegree ((X + 1) : Nat[X]) ≤ 1 := by hint -- "hint" now correctly suggests "field_simp" which closes the goal (no closing tactic suggested prior to this PR) example (R : Type) (a b : R) [CommRing R] (u₁ : Rˣ) : a /ₚ u₁ + b /ₚ u₁ = (a + b) /ₚ u₁ := by hint -- "hint" now correctly suggests "finiteness" which closes the goal (no closing tactic suggested prior to this PR) example (a : ℝ) : (ENNReal.ofReal (1 + a ^ 2))⁻¹ < ⊤ := by hint ```
…cing binders (leanprover-community#25716) This PR adds @[gcongr] tags so that - `gcongr` can move inside Eventually and Frequently, - moving inside of `∀ ε > 0,` or `∃ ε > 0,` adds the hypothesis/condition to the local context.
This PR defines `RefinedDiscrTree`, which is an improved version of `DiscrTree` with many new features, such as - indexing lambda terms, dependent forall terms, and bound variables. - giving a score to matches, in order to sort them - indexing star patterns so that `a+b` and `a+a` are indexed differently - taking into account eta reductions, so that `exp` can still be matched with the library pattern `fun x => exp (f x)`. This PR makes `RefinedDiscrTree` into a lazy data structure, meaning that it can be used without a cache, just like `LazyDiscrTree`. This PR also removes these features: - indexing `fun x => x` as `id` - indexing `fun x => f x + g x` as `f + g`, and similarly for `-`, `*`, `/`, `⁻¹`, `^`. - indexing `fun _ => 42` as `42` These equivalent indexings do not hold definitionally in the `reducible` transparency, which is the transparency that is used for unification when using a discrimination tree. Therefore, indexing these different expressions the same is actually inefficient rather than helpful. This is part of the bigger leanprover-community#11768, which uses this discrimination tree for a library rewriting tactic. This replaces an older version of `RefinedDiscrTree`. Co-authored-by: JovanGerb <56355248+JovanGerb@users.noreply.github.com>
Fixes an issue I encountered on windows where `IO.Process.run { cmd := "date", args := #["-I"] }` exits with an error `no such file or directory (error code: 2)`, making this tactic unusable.
…munity#25792) Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
github-actions
Bot
added
the
merge-conflict
Contributor
Author
|
Something went wrong when migrating to fork. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
20 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
feat (Topology/Compactness/CompactSystem): Closed and compact square cylinders form a
compact system.
A square cylinder is a set of the form
s.pi tin a product space. A closed compact square cylinder hasIsClosed (t i)andIsCompact (t i)for alli ∈ s. This set system is a compact system (as introduced in PR #24541).Streamline the definition of square cylinders in MeasureTheory/Constructions/Cylinders on the way.
Co-authors: Rémy Degenne remy.degenne@inria.fr
This PR continues the work from #24542.
Original PR: #24542