PR #2069 feat(topology): is_closed_proj_of_compact

feat(topology): is_closed_proj_of_compact #2069

mergify merged 13 commits into master from kevin-compact

feat(lattice): add inf_le_inf_left/right

49b85a4a

feat(set/lattice): image_inter_subset

a84d7b18

feat(set/lattice): push_pull

f422b498

feat(order/filter): push_pull and product notation

44801296

feat(topology/subset_properties): is_closed_proj_of_compact

226947b3

feat(set/lattice): push_pull'

50cd85fa

fix(order/filter): forgotten doc

91c3930c

PatrickMassot changed the title ~~Kevin compact~~ is_closed_proj_of_compact 6 years ago

lint (including old missing docstrings in filter).

33cdadb2

PatrickMassot changed the title ~~is_closed_proj_of_compact~~ feat(topology): is_closed_proj_of_compact 6 years ago

urkud commented on 2020-03-01

urkud added awaiting-author

cipher1024 assigned

urkud 6 years ago

Apply Yury's suggestions.

0065a73c

Forgotten style fix

78c162ae

PatrickMassot removed awaiting-author

PatrickMassot added awaiting-review

urkud commented on 2020-03-11

urkud's suggestions

853d5d72

kim-em commented on 2020-03-11

kim-em approved these changes on 2020-03-11

kim-em removed awaiting-review

kim-em added ready-to-merge

Update src/order/filter/basic.lean

df9d5456

Merge branch 'master' into kevin-compact

20cb65d0

mergify merged 1b0a7493 into master 6 years ago

mergify deleted the kevin-compact branch 6 years ago

Reviewers

kim-em

urkud

Assignees

urkud

Labels

ready-to-merge

Milestone

No milestone

mathlib3 feat(topology): is_closed_proj_of_compact #2069 Merged

feat(topology): is_closed_proj_of_compact #2069

mathlib3
feat(topology): is_closed_proj_of_compact
#2069

Merged