Skip to content

[Merged by Bors] - chore(Topology/Constructions): rename most type variables #9863

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 12 commits into from
Closed

[Merged by Bors] - chore(Topology/Constructions): rename most type variables #9863

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
032a9f7
Replace \alpha by X.
grunweg Jan 20, 2024
a70959e
automatic: rename \beta to Y; two build errors to fix
grunweg Jan 20, 2024
e54ae45
Manual: rename \beta to Y, and fix some renaming mishaps from the \al…
grunweg Jan 20, 2024
f56f69b
Rename \gamma to Z.
grunweg Jan 20, 2024
c79d63d
Rename topological spaces \gamma to Z.
grunweg Jan 20, 2024
9982eb2
Rename a subset of X from \gamma to t.
grunweg Jan 20, 2024
51894b3
Rename collection \rho i of top. space to X i.
grunweg Jan 20, 2024
dc8044e
Fix build.
grunweg Jan 20, 2024
b0f3b0a
Review comments, and make the same change in one more place.
grunweg Jan 24, 2024
a0e1b74
Use \oplus for the Sum of two topological spaces.
grunweg Jan 24, 2024
97d30c4
Last review comments:
grunweg Jan 25, 2024
658b871
Rename further occurrences of a : X and b : Y to x : X and y : Y.
grunweg Jan 25, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions Mathlib/CategoryTheory/Extensive.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -387,7 +387,7 @@ instance finitaryExtensive_TopCat : FinitaryExtensive TopCat.{u} := by
refine' ⟨⟨l, _⟩, ContinuousMap.ext fun a => (hl a).symm, TopCat.isTerminalPUnit.hom_ext _ _,
fun {l'} h₁ _ => ContinuousMap.ext fun x =>
hl' x (l' x) (ConcreteCategory.congr_hom h₁ x).symm⟩
apply (embedding_inl (α := X') (β := Y')).toInducing.continuous_iff.mpr
apply (embedding_inl (X := X') (Y := Y')).toInducing.continuous_iff.mpr
convert s.fst.2 using 1
exact (funext hl).symm
· refine' ⟨⟨hαY.symm⟩, ⟨PullbackCone.isLimitAux' _ _⟩⟩
Expand All @@ -404,7 +404,7 @@ instance finitaryExtensive_TopCat : FinitaryExtensive TopCat.{u} := by
refine' ⟨⟨l, _⟩, ContinuousMap.ext fun a => (hl a).symm, TopCat.isTerminalPUnit.hom_ext _ _,
fun {l'} h₁ _ =>
ContinuousMap.ext fun x => hl' x (l' x) (ConcreteCategory.congr_hom h₁ x).symm⟩
apply (embedding_inr (α := X') (β := Y')).toInducing.continuous_iff.mpr
apply (embedding_inr (X := X') (Y := Y')).toInducing.continuous_iff.mpr
convert s.fst.2 using 1
exact (funext hl).symm
· intro Z f
Expand Down
Loading