In mathlib, topological properties are generally characterized in terms of filters wherever possible. In particular, a set $K$ is said to be compact provided that for every nontrivial filter $F$ that contains $K$, there exists a point $k\in K$ such that every set of $F$ meets every neighborhood of $k$. This is then proven to be equivalent to the usual covers-have-finite-subcovers property. Similarly, Lindelöf spaces are defined using filters, then proven to covers-have-countable-subcovers.

A pending pull request https://github.com/leanprover-community/mathlib4/pull/11800 aims to add $\kappa$-Lindelöf by this filter definition:

Say a $\kappa$-filter is a filter $F$ for which $G\in[F]^{<\kappa}$ implies $\bigcap G\in F$. A set $S$ is $\kappa$-Lindelöf if every nontrivial $\kappa$-filter that contains $S$ has a point $s\in K$ such that every set of $F$ meets every neighborhood of $s$.

Is this equivalent to the following covering property definition?

A set $S$ is $\kappa$-Lindelöf if every open cover has a subcover of cardinality $<\kappa$.

In particular, the pull request proves this equivalence for the case $\kappa$ is regular. Is this assumption necessary?

In mathlib, topological properties are generally characterized in terms of filters wherever possible. In particular, a set $K$ is said to be compact provided that for every nontrivial filter $F$ that contains $K$, there exists a point $k\in K$ such that every set of $F$ meets every neighborhood of $k$. This is then proven to be equivalent to the usual covers-have-finite-subcovers property. Similarly, Lindelöf spaces are defined using filters, then proven to covers-have-countable-subcovers.

A pending pull request https://github.com/leanprover-community/mathlib4/pull/11800 aims to add $\kappa$-Lindelöf by this filter definition:

Say a $\kappa$-filter is a filter $F$ for which $G\in[F]^{<\kappa}$ implies $\bigcap G\in F$. A set $S$ is $\kappa$-Lindelöf if every nontrivial $\kappa$-filter that contains $S$ has a point $s\in S$ such that every set of $F$ meets every neighborhood of $s$.

Is this equivalent to the following covering property definition?

A set $S$ is $\kappa$-Lindelöf if every open cover has a subcover of cardinality $<\kappa$.

In particular, the pull request proves this equivalence for the case $\kappa$ is regular. Is this assumption necessary?

In mathlib, topological properties are generally characterized in terms of filters wherever possible. In particular, a set $K$ is said to be compact provided that for every nontrivial filter $F$ that contains $K$, there exists a point $k\in K$ such that every set of $F$ meets every neighborhood of $k$. This is then proven to be equivalent to the usual covers-have-finite-subcovers property. Similarly, Lindelöf spaces are defined using filters, then proven to covers-have-countable-subcovers.

A pending pull request https://github.com/leanprover-community/mathlib4/pull/11800 aims to add $\kappa$-Lindelöf by this filter definition:

Say a $\kappa$-filter is a filter $F$ for which $G\in[F]^{<\kappa}$ implies $\bigcap G\in F$. A set $S$ is $\kappa$-Lindelöf if every nontrivial $\kappa$-filter that contains $S$ has a point $s\in K$ such that every set of $F$ meets every neighborhood of $s$.

Is this equivalent to the following covering property definition?

A set $S$ is $\kappa$-Lindelöf if every open cover has a subcover of cardinality $\leq\kappa$.

In particular, the pull request proves this equivalence for the case $\kappa$ is regular. Is this assumption necessary?

In mathlib, topological properties are generally characterized in terms of filters wherever possible. In particular, a set $K$ is said to be compact provided that for every nontrivial filter $F$ that contains $K$, there exists a point $k\in K$ such that every set of $F$ meets every neighborhood of $k$. This is then proven to be equivalent to the usual covers-have-finite-subcovers property. Similarly, Lindelöf spaces are defined using filters, then proven to covers-have-countable-subcovers.

A pending pull request https://github.com/leanprover-community/mathlib4/pull/11800 aims to add $\kappa$-Lindelöf by this filter definition:

Say a $\kappa$-filter is a filter $F$ for which $G\in[F]^{<\kappa}$ implies $\bigcap G\in F$. A set $S$ is $\kappa$-Lindelöf if every nontrivial $\kappa$-filter that contains $S$ has a point $s\in K$ such that every set of $F$ meets every neighborhood of $s$.

Is this equivalent to the following covering property definition?

A set $S$ is $\kappa$-Lindelöf if every open cover has a subcover of cardinality $<\kappa$.

In particular, the pull request proves this equivalence for the case $\kappa$ is regular. Is this assumption necessary?