basic): add `rel_covering`, golf
#18128

Open

feat(order/rel_iso/basic): add `rel_covering`, golf #18128

astrainfinita wants to merge 25 commits into master from FR_rel_iff

feat(order/rel_iso/basic): add typeclasses and structure, golf

f8250eab

astrainfinita added WIP

astrainfinita added RFC

astrainfinita added awaiting-CI

fix

27b7ceba

fix

e5163677

Update noetherian_space.lean

419bab81

fix

5240e73f

convenience lemmas

96349479

reduce diffs

c9c8066a

`rel_covering` is better? remove `rel_iff_class`

afcd179e

more removing

7fce8da9

fix

d52fb3fa

astrainfinita requested a review 2 years ago

fix lint

81bef5bd

fix

b8aea421

remove `rel_reflecting_class` `rel_iff_hom`

790b0224

reduce diffs

2153acf2

astrainfinita changed the title ~~feat(order/rel_iso/basic): add typeclasses and structure, golf~~ feat(order/rel_iso/basic): add `rel_covering`, golf 2 years ago

github-actions removed awaiting-CI

golf

7e516e59

fix docstr

930b19f0

astrainfinita removed WIP

astrainfinita removed RFC

astrainfinita added awaiting-review

astrainfinita added t-order

astrainfinita added mathlib4-pair

fix docstr

8978325d

implicit

e2c19d8a

Merge branch 'master' into FR_rel_iff

fb899afb

golf

445803f4

Merge branch 'master' into FR_rel_iff

ce92d5ee

feat(order/rel_iso/basic): add `rel_covering`, defs only

f128d4be

Merge branch 'FR_rel_covering' into FR_rel_iff

013dd651

mathlib-dependent-issues-bot added blocked-by-other-PR

YaelDillies removed mathlib4-pair

Merge branch 'master' into FR_rel_iff

b1688d5b

Update basic.lean

e5f183f2

eric-wieser added not-too-late

Reviewers

No reviews

Assignees

No one assigned

Labels

awaiting-review blocked-by-other-PR t-order not-too-late

Milestone

No milestone

mathlib3 feat(order/rel_iso/basic): add `rel_covering`, golf #18128 Open

feat(order/rel_iso/basic): add `rel_covering`, golf #18128

mathlib3
feat(order/rel_iso/basic): add `rel_covering`, golf
#18128

Open