# Zulip Chat Archive

## Stream: PR reviews

### Topic: 3083 finset lattice

#### Yury G. Kudryashov (Jun 15 2020 at 20:24):

#3083 makes `finset`

use `lattice`

operations instead of "set" operations. What do you think about this? `data.finset`

now compiles but I don't want to waste time on porting the rest of `mathlib`

if this is not going to be merged.

#### Bhavik Mehta (Jun 15 2020 at 20:27):

What's the advantage of this? I think it would be slightly more confusing for newbies who want to use finsets but don't want to think about a lattice, and if I remember correctly the lattice operations already work on finsets anyway

#### Chris Hughes (Jun 15 2020 at 20:30):

I think it's a good idea. It just means you don't need duplicates of all lemmas on lattice operations and set operations. Occasionally I can't `rw`

with a lattice lemma because I've got set operations or vice versa.

#### Patrick Massot (Jun 15 2020 at 20:51):

Does it mean you want to use the obscure lattice notations for set/finset intersection and union?

#### Patrick Massot (Jun 15 2020 at 20:52):

If you want to unify everything I would rather drop the lattice notations and use round intersection and union everywhere instead of the lattice square versions

#### Patrick Massot (Jun 15 2020 at 20:52):

Oh I see Gabriel also likes round notations.

#### Patrick Massot (Jun 15 2020 at 20:54):

Either way it sounds like a drastic change that is not drastically motivated.

#### Patrick Massot (Jun 15 2020 at 20:55):

I would very much prefer having integrals that work.

#### Kevin Buzzard (Jun 15 2020 at 21:07):

We have the zany lattice notation for ideals and I got used to it in the end. There are advantages of a unified approach. I get annoyed that set.preimage isn't called comap nowadays

#### Yury G. Kudryashov (Jun 15 2020 at 21:25):

I was thinking about definitions, not notation.

#### Yury G. Kudryashov (Jun 15 2020 at 21:27):

The only question about using `∪`

ant `∩`

for lattice is what to do with `≤`

/`<`

/`⊥`

vs `⊆`

/`⊂`

/`∅`

.

#### Yury G. Kudryashov (Jun 15 2020 at 21:28):

I know only one type with different interpretation of `≤`

and `⊆`

: `multiset`

.

#### Scott Morrison (Jun 15 2020 at 23:09):

I think having any types with both `≤`

and `⊆`

is probably a bad idea: just a recipe for confusion. (I remember being dismayed stumbling on this one.) I would propose picking the important one to receive notation (whether it's `≤`

and `⊆`

) and just dealing with being more verbose for the other.

#### Jeremy Avigad (Jun 16 2020 at 01:05):

Whenever I have to do anything with lattices I struggle a lot with typing `\lub`

and `\glb`

because I have to mentally reconstruct which is which. It doesn't help that we think of them as `union`

and `inter`

, and the lattice names are `sup`

and `inf`

. Maybe it would help if we could also use `\lunion`

and `\linter`

for "lattice union" and "lattice inter", or something like that.

#### Mario Carneiro (Jun 16 2020 at 01:27):

what about `\sqcap`

and `\sqcup`

?

#### Jeremy Avigad (Jun 16 2020 at 01:36):

Yeah, that works for me.

#### Kevin Buzzard (Jun 16 2020 at 01:36):

I must confess I feel the same as Jeremy about these funny words. I guess I recognise cup as union though

#### Jeremy Avigad (Jun 16 2020 at 02:42):

Oh, yeah, and when talking about lattices in ordinary mathematics I use "meet" and "join." We give the dictionary here: https://avigad.github.io/mathematics_in_lean/basics.html#proving-facts-about-algebraic-structures

I put the translations there to help myself sort them out more than anyone else.

#### Yury G. Kudryashov (Jun 16 2020 at 03:02):

Changing `sup`

to `join`

and `inf`

to `meet`

should not be too hard.

#### Yury G. Kudryashov (Jun 16 2020 at 03:02):

But I don't want to start any of these refactors until we'll agree on the goal.

#### Johan Commelin (Jun 16 2020 at 06:38):

I would like to maintain readability as much as possible. But uniformity pays off in the long run. And I think the symbols are similar enough that we can explain to anyone that `\sqcup`

is the symbol for union of "set-like" things. Then we only need to tell them that in names

`subset`

becomes`le`

`union`

becomes`meet`

`inter`

becomes`join`

and I think all of those are pretty self-explanatory.

The hardest thing might be`empty`

becomes`bot`

...

And of course`univ`

was already confusing to begin with, so replacing it with`top`

doesn't change anything. (-;

#### Yury G. Kudryashov (Jun 16 2020 at 06:40):

We can use union and inter for meet and join though in some contexts (e.g., `supr`

in `real`

s or `ennreal`

s) this looks funny.

#### Gabriel Ebner (Jun 16 2020 at 07:10):

Jeremy Avigad said:

I use "meet" and "join."

I mix up meet and join ~~pretty often~~ always, I guess mostly because these words don't exist in German. In German we typically use supremum and infimum, so I prefer the current naming.

#### Gabriel Ebner (Jun 16 2020 at 07:19):

Yury G. Kudryashov said:

in some contexts [...] this looks funny.

$\sqrt{2} \cup \pi = \pi$ doesn't look so bad, it reminds me of Dedekind cuts.

#### Jeremy Avigad (Jun 16 2020 at 11:34):

I didn't mean to suggest that `meet`

and `join`

are better than `sup`

and `inf`

. It would help if we could reclaim `\sup`

and `\inf`

in VS Code. We already have `\supseteq`

and `\infty`

for the symbols they are assigned to now. It might help to be able to type `\sqcap`

and `\sqcup`

when working with finsets, because `\cap`

and `\cup`

are used in Latex for intersections and unions. But I can probably get used to the fact that intersection is `\inf`

because it is smaller and union is `\sup`

because it is bigger. It's just that `\glb`

and `\lub`

are horrible, because e.g. "greatest" and "lower" go in opposite directions, and I have to stop to think about which one wins.

#### Johan Commelin (Jun 16 2020 at 17:28):

Gabriel Ebner said:

Yury G. Kudryashov said:

in some contexts [...] this looks funny.

$\sqrt{2} \cup \pi = \pi$ doesn't look so bad, it reminds me of Dedekind cuts.

I guess this is tongue in cheek? I'm not a fan :wink: I guess that for linear orders we want to simp this away to `max a b`

as soon as possible?

#### Gabriel Ebner (Jun 16 2020 at 17:34):

I'm 60% serious. $\sqrt{2} \sqcup \pi = \pi$ doesn't look any better to me. But $1 \in \pi$ would be too much, even for me.

#### Johan Commelin (Jun 16 2020 at 17:35):

Gabriel Ebner said:

I'm 60% serious. $\sqrt{2} \sqcup \pi = \pi$ doesn't look any better to me.

But it also doesn't look any worse, right? (At least to me...)

#### Gabriel Ebner (Jun 16 2020 at 17:36):

I completely agree. That's why I think ${}\cup{}$ is the best choice if we want to standardize, because it looks right half of the time (with sets, multisets, etc.).

#### Johan Commelin (Jun 16 2020 at 17:36):

But on an abstract lattice, it looks "wrongish".

#### Johan Commelin (Jun 16 2020 at 17:37):

And the problem remains with `\le`

vs `\subset`

, right?

#### Johan Commelin (Jun 16 2020 at 17:37):

We definitely don't want `0 \subset 1`

.

#### Gabriel Ebner (Jun 16 2020 at 17:38):

Yes, `⊆`

vs. `≤`

is the hard one. How about `∅ ≤ A ∩ B`

? *ducks*

#### Johan Commelin (Jun 16 2020 at 17:42):

I think I prefer to go full lattice notation everywhere.

#### Reid Barton (Jun 16 2020 at 17:52):

$\cup$/$\cap$ look really wrong when they are wrong, for example, filters ordered by reverse inclusion.

#### Scott Morrison (Jun 17 2020 at 04:47):

Is it insane to have all the notations mean the same thing (i.e. lattice operations), and let people use different ones in different contexts?

#### Yury G. Kudryashov (Jun 17 2020 at 04:50):

Proof state will always use one notation.

#### Bryan Gin-ge Chen (Jun 17 2020 at 05:03):

Is this sort of thing why we have to prove everything for both additive groups and multiplicative groups?

#### Yury G. Kudryashov (Jun 17 2020 at 05:05):

For multiplicative and additive groups we also have rings. They use both multiplicative and additive structures.

#### Yury G. Kudryashov (Jun 17 2020 at 05:06):

One possible solution is to write a `to_additive`

-style attribute and add it to all the `lattice`

lemmas.

#### Yury G. Kudryashov (Jun 17 2020 at 05:07):

But then we'll have to decide which notation is better in each case.

#### Floris van Doorn (Jun 26 2020 at 22:45):

I wouldn't mind using lattice notation everywhere.

I'm not in favor using set notation for lattices.

The current status quo means we have to redo everything about lattices separately for sets and finsets, which is not great. There have been plenty of cases where I needed a lemma that existed for exactly one of {bUnion, supr} and I needed it for the other one.

#### Yury G. Kudryashov (Jun 26 2020 at 23:30):

Even worse, we need to redo lots of stuff separately for sets, finsets, and lattices.

#### Yury G. Kudryashov (Jun 29 2020 at 19:25):

Let me revive this thread. What are the reasons **against** migration of `set`

s, `multiset`

s and `finset`

s to `lattice`

?

#### Yury G. Kudryashov (Jun 29 2020 at 19:26):

I remember the following:

- $\sqcup$ and $\sqcap$ look worse than $\cup$ and $\cap$;
- it's hard to remember
`\lub`

for $\sqcup$.

What else?

#### Johan Commelin (Jun 29 2020 at 19:28):

The second point is no longer valid after all the new additions to the translations file.

#### Floris van Doorn (Jun 29 2020 at 19:28):

point 2 has been resolved: there are now many ways to input `⊔`

and `⨆`

.

I think a point that is close to point 1: lattice notation is beginner unfriendly.

#### Yury G. Kudryashov (Jun 29 2020 at 19:30):

And defining $f'(x)$ using normed spaces and filters is very beginner friendly ;)

#### Yury G. Kudryashov (Jun 29 2020 at 19:31):

BTW, when I first saw Lean the fact that `⊂`

means $\subsetneq$ was very surprising.

#### Floris van Doorn (Jun 29 2020 at 19:31):

There is a difference: with a good enough API you don't need to know about normed spaces & filters to work with the derivative on functions `real -> real`

. The lattice operations on `set`

**is** the API.

(just to be clear: I'm in favor of using lattice notation for sets over the status quo)

#### Sebastien Gouezel (Jun 29 2020 at 19:35):

Can we have `local notation : ∪ := ⊔`

, and use it in the set files?

#### Sebastien Gouezel (Jun 29 2020 at 19:36):

Or even have it globally as an input notation in all files?

#### Floris van Doorn (Jun 29 2020 at 19:37):

I'm afraid that might make things even more confusing if the lemmas you use are called `sup_comm`

and `image_sup`

(or `sup_comm`

and `image_union`

??).

#### Johan Commelin (Jun 29 2020 at 19:38):

`image`

and `preimage`

should *clearly* be renamed to `map`

and `comap`

... ...

... :confused: :rolling_on_the_floor_laughing:

#### Sebastien Gouezel (Jun 29 2020 at 19:39):

Floris van Doorn said:

I'm afraid that might make things even more confusing if the lemmas you use are called

`sup_comm`

and`image_sup`

(or`sup_comm`

and`image_union`

??).

Good point!

#### Floris van Doorn (Jun 29 2020 at 19:41):

Also, what does `s ≤ t`

mean to a mathematician (if anything)? Is it pointwise inequalities: `∀ x ∈ s, ∀ y ∈ t, x ≤ y`

? Using lattice notation means that it has to mean `subset`

...

#### Johan Commelin (Jun 29 2020 at 19:44):

I guess it *could* mean pointwise ineqs, but I think that's very rare.

#### Alex J. Best (Jun 29 2020 at 19:44):

I don't think the idea that sets form a partial order w.r.t. inclusion is so alien to mathematicians, so I'd say most would guess it means subset.

#### Johan Commelin (Jun 29 2020 at 19:46):

It definitely helps that the lattice notation is just a pointy-squary version of the set notation.

#### Floris van Doorn (Jun 29 2020 at 19:50):

But it might take some time to get used to names like `le_image_sup : f '' (s ⊔ f ⁻¹' t) ≤ f '' s ⊔ t`

(or `le_map_sup`

). I do feel like we're losing something when moving from the current notation/naming to the lattice versions...

#### Sebastien Gouezel (Jun 29 2020 at 19:53):

We would need an attribute like `to_additive`

to create `union`

lemmas from `sup`

lemmas, and a notation `union = sup`

. Then it would be mostly transparent to the user, but with better defeq properties.

#### Jeremy Avigad (Jun 29 2020 at 19:53):

How about having something like the `to_additive`

trick, so that we can batch-duplicate lattice theorems with set names and set notation (for types that have that notation defined)?

#### Sebastien Gouezel (Jun 29 2020 at 19:53):

I was faster :)

#### Alex J. Best (Jun 29 2020 at 19:53):

As a small experiment, I just asked two grad students (in number theory) what `X \le Y`

for `X, Y`

sets means with no hints, one guessed the partial order by inclusion, and one guessed an inequality of cardinals (i.e. exists an injection from `X \to Y`

. It might have been more realistic to pose it as `X, Y`

subsets of `Z`

, what does `X\le Y`

mean.

#### Yury G. Kudryashov (Jun 29 2020 at 19:55):

If we try the `to_additive`

trick, then which notation should we use for `submonoid`

s etc?

#### Sebastien Gouezel (Jun 29 2020 at 19:58):

I would say: don't touch existing files. Both notations should be completely equivalent, so you can even use `\le`

at one line and `\subseteq`

at the next one.

#### Floris van Doorn (Jun 29 2020 at 19:58):

I guess lattice operations are fine on `submonoids`

, `opens`

, ...

For submonoids you don't even have `↑(s ⊔ t) = ↑s ∪ ↑t`

in general

#### Floris van Doorn (Jun 29 2020 at 20:00):

@Sebastien Gouezel As an temporary solution? Eventually we will want to name our lemmas in a consistent way (which probably means using `_sup_`

instead of `_union_`

everywhere)

#### Floris van Doorn (Jun 29 2020 at 20:01):

But if we use `∪`

for set, we probably also want it for `finset`

...

#### Johan Commelin (Jun 29 2020 at 20:01):

I think that @Sebastien Gouezel is proposing to throw away `set/basic.lean`

and instead tag every lemma in `order/lattice.lean`

with `@[to_set]`

.

#### Sebastien Gouezel (Jun 29 2020 at 20:01):

Exactly.

#### Sebastien Gouezel (Jun 29 2020 at 20:03):

In more specialized domains, we should settle on one of the choices. I'd say use union and subset for sets and finsets (and more generally if there is a coercion to sets satisfying `coe (a sup b) = coe a union coe b`

), and order notation otherwise.

#### Floris van Doorn (Jun 29 2020 at 20:04):

is the statement of lemma `union_comm`

the same as `sup_comm`

, or is it specialized to sets?

#### Sebastien Gouezel (Jun 29 2020 at 20:05):

It is exactly the same statement.

#### Sebastien Gouezel (Jun 29 2020 at 20:05):

(Possibly with a different pretty printer setting so that the sup is shown as a union in the tooltip)

#### Floris van Doorn (Jun 29 2020 at 20:06):

ah ok. that would make it easier.

#### Floris van Doorn (Jun 29 2020 at 20:06):

yeah, you probably still want different `has_union`

and `has_sup`

classes, and let `to_set`

modify the classes as well, so that the goal/lemmas are printed the way you wrote them.

I guess that could work.

#### Kevin Buzzard (Jun 29 2020 at 20:07):

@Alex J. Best I agree: if you don't know X and Y are subsets of Z then $X\subseteq Y$ doesn't make much sense. If they're both subsets of Z then there's at most one canonical injection from X to Y and so now you're more likely to guess the inclusion.

#### Johan Commelin (Jun 29 2020 at 20:08):

This is going to be a refactor so big that :head_bandage: :head_bandage: :head_bandage:

#### Alex J. Best (Jun 29 2020 at 20:08):

I agree, it was a flawed experiment! But someone still got it right!

#### Yury G. Kudryashov (Jun 29 2020 at 20:17):

If we have different `has_sup`

and `has_union`

classes, then how can `union_comm`

and `sup_comm`

be the same?

#### Sebastien Gouezel (Jun 29 2020 at 20:18):

I think we should just have one class.

#### Yury G. Kudryashov (Jun 29 2020 at 20:19):

Then what should `@[to_set]`

do?

#### Yury G. Kudryashov (Jun 29 2020 at 20:19):

And I guess we won't be able to tell pretty-printer to consistently use `∪`

for sets and finsets.

#### Sebastien Gouezel (Jun 29 2020 at 20:21):

```
@[to_set] theorem le_sup_right : b ≤ a ⊔ b
```

should create a theorem `subset_union_right`

which is defeq to `le_sup_right`

, but in which `notation union := sup`

and `notation subseteq := \le`

are activated so that the tooltip shows right.

#### Sebastien Gouezel (Jun 29 2020 at 20:22):

Yury G. Kudryashov said:

And I guess we won't be able to tell pretty-printer to consistently use

`∪`

for sets and finsets.

I agree, but I think this is only a minor annoyance. (And it might be solvable in Lean 4).

#### Yury G. Kudryashov (Jun 29 2020 at 20:25):

What do you mean by "notation ... are activated"? AFAIK, Lean doesn't store notation with lemma statements. It uses currently active notation in `#print`

etc.

#### Floris van Doorn (Jun 29 2020 at 20:25):

Yury G. Kudryashov said:

If we have different

`has_sup`

and`has_union`

classes, then how can`union_comm`

and`sup_comm`

be the same?

with two different classes, they are not syntactically equal.

My idea (to get the pretty printing right) is to have separate `has_sup`

and `has_union`

classes. Given a `lattice`

you have instances to both `has_sup`

and `has_union`

, and the underlying maps are definitionally equal.

Then `@[to_set]`

replaces all `sup`

s with `union`

s, in the same way that `to_additive`

does it.

#### Floris van Doorn (Jun 29 2020 at 20:25):

The lemmas will be definitionally equal, but not syntactically equal.

#### Sebastien Gouezel (Jun 29 2020 at 20:26):

Yury G. Kudryashov said:

What do you mean by "notation ... are activated"? AFAIK, Lean doesn't store notation with lemma statements. It uses currently active notation in

ok, too bad

#### Yury G. Kudryashov (Jun 29 2020 at 20:27):

If we use different classes, why should we care about `defeq`

? We can make `@[to_set]`

do the same as `@[to_additive]`

.

#### Floris van Doorn (Jun 29 2020 at 20:29):

we don't necessarily care about defeq.

#### Sebastien Gouezel (Jun 29 2020 at 20:32):

I don't remember the start of the thread: wasn't your goal to get union defeq to to \sup to start with?

#### Yury G. Kudryashov (Jun 29 2020 at 20:33):

Let's say we consider different options. The goal is to reduce code duplication.

#### Yury G. Kudryashov (Jun 29 2020 at 20:34):

Currently we prove quite a few `lattice`

lemmas for (a) `set`

s; (b) `finset`

s; (c) all other lattices.

#### Yury G. Kudryashov (Jun 29 2020 at 20:36):

Technically the simplest solution is to start using `≤`

, $\sqcap$ etc everywhere but this is bad for new users.

#### Yury G. Kudryashov (Jun 29 2020 at 20:41):

Other solutions include: (a) use a `@[to_additive]`

-like attribute to transfer lemmas from `lattice`

operations to `set`

operations; (b) allow `∪`

as a (local?) alternative syntax for $\sqcup$ and use it for `set`

s and `finset`

s.

#### Sebastien Gouezel (Jun 29 2020 at 20:42):

From the discussion, (a) looks like the nicest solution, albeit not the easiest to implement.

#### Yury G. Kudryashov (Jun 29 2020 at 20:44):

The main drawback of (a) is that we'll need class names for `set`

versions of everything up to `complete_boolean_algebra`

and, e.g., `monotone`

won't work automatically unless we define `has_le`

as well.

#### Yury G. Kudryashov (Jun 29 2020 at 20:45):

I hope that with Lean 4 we'll be able to define a pretty-printer that uses `∪`

for some types and $\sqcup$ for all other types.

#### Yury G. Kudryashov (Jun 29 2020 at 20:48):

So we have option (c): wait for Lean 4.

#### Sebastien Gouezel (Jun 29 2020 at 20:50):

Even with Lean 4, we would need `@[to_set]`

to create lemma names with union and subset instead of sup and le.

#### Jeremy Avigad (Jun 29 2020 at 20:51):

Is it a problem that `order.complete_lattice`

depends on properties of sets, through `order.bounds`

? On a quick look, `order.bounds`

only uses finite unions and intersections, subset, empty and univ. So maybe it is o.k.

#### Yury G. Kudryashov (Jun 29 2020 at 20:52):

It's easy to reorder `import`

s so that `data/set/basic`

will know the *definition* of `complete_boolean_algebra`

and *lemmas* about `bounded_lattice`

.

#### Yury G. Kudryashov (Jun 29 2020 at 21:00):

(done locally)

#### Yury G. Kudryashov (Jun 29 2020 at 21:01):

Sebastien Gouezel said:

Even with Lean 4, we would need

`@[to_set]`

to create lemma names with union and subset instead of sup and le.

It's easier to add `alias`

es with custom names than to modify types.

#### Johan Commelin (Jun 30 2020 at 04:31):

Yury G. Kudryashov said:

The main drawback of (a) is that we'll need class names for

`set`

versions of everything up to`complete_boolean_algebra`

and, e.g.,`monotone`

won't work automatically unless we define`has_le`

as well.

Well, `to_set`

wouldn't have to replay the proofs (like `to_additive`

) does, if we make sure that things are defeq. Then it just has to modify the name and statement, and can prove the resulting lemma by directly calling the lattice version.

So it generates

```
lemma subset_union_right : the-statement :=
le_sup_right _ _ _
```

To make this work, we have to give `set`

some low-priority `has_le`

and `has_sup`

instances, but it would save us from duplicating the entire lattice class hierarchy for set-like notation.

#### Yury G. Kudryashov (Jun 30 2020 at 06:54):

What's wrong with the approach "make `\cup`

and `\sqcup`

two notations for the same operation and make `@[to_set]`

work as `alias + autogen name`

"? This way we can't have good notation in the proof state but we can be sure that any lemma about `lattice`

s work for `set`

s even without a `@[to_set]`

alias.

#### Yury G. Kudryashov (Jun 30 2020 at 06:55):

We still can have good notation in the input.

#### Yury G. Kudryashov (Jun 30 2020 at 06:55):

(and I hope that we'll be able to have a good notation in the proof state in Lean 4)

#### Yury G. Kudryashov (Jun 30 2020 at 07:06):

How exactly should the "defeq" based `@[to_set]`

work? Should we add some instances like `has_subset.to_has_le`

and use them when transforming the statement? Will it play nice with diamonds?

#### Sebastien Gouezel (Jun 30 2020 at 07:09):

Shouldn't we remove completely `has_subset`

, and use subset as a notation for le?

#### Yury G. Kudryashov (Jun 30 2020 at 07:12):

With the "make `\cup`

and `\sqcup`

two notations for the same operation" approach yes, we should. But I'm trying to understand what other options do we have, and can't understand the "defeq" approach @Johan Commelin is talking about.

#### Kevin Buzzard (Jun 30 2020 at 07:22):

Sebastien Gouezel said:

Shouldn't we remove completely

`has_subset`

, and use subset as a notation for le?

Shouldn't we completely remove `has_mul`

, and use `*`

as a notation for `has_add`

?

#### Kevin Buzzard (Jun 30 2020 at 07:23):

I guess there might be some edge cases where a type has two monoid structures

#### Yury G. Kudryashov (Jun 30 2020 at 14:36):

@Kevin Buzzard Let's discuss lattices, not monoids. Currently there is only one rarely used type (`multiset`

) with both `has_subset`

and `has_le`

and `has_le.le ≠ has_subset.subset`

.

#### Kevin Buzzard (Jun 30 2020 at 14:42):

So rather fewer edge cases than in the */+ case.

#### Yury G. Kudryashov (Jun 30 2020 at 14:57):

And I'm not aware of good structures involving `has_subset`

on `multiset`

, so we can just add a custom notation for this.

#### Yury G. Kudryashov (Jun 30 2020 at 16:29):

One more type with sensible `has_subset`

different from `has_le`

: `list`

.

#### Gabriel Ebner (Jun 30 2020 at 16:33):

IIRC there is more than one reasonable (non-subset) definition of `≤`

on lists. And only one of them is well-founded (if the order on the elements is well-founded). Maybe these should be different relations (i.e., not `≤`

) anyhow.

Last updated: May 09 2021 at 13:20 UTC