English
For a well-reflexive relation r on α, c ≤ cof r iff for every set S with the property that every a has some b ∈ S with r a b, we have c ≤ |S|.
Русский
Для хорошо-замкнутого отношения r на α верно: c ≤ cof r тогда и только тогда, когда для любого множества S, удовлетворяющего условию ∀ a ∃ b ∈ S: r a b, выполняется c ≤ |S|.
LaTeX
$$$c \\le cof(r) \\leftrightarrow \\forall \\{S : Set\\, \\alpha\\}, (\\forall a, \\exists b \\in S, r\,a\,b) \\rightarrow c \\le |S|$$$
Lean4
theorem le_cof [IsRefl α r] (c : Cardinal) : c ≤ cof r ↔ ∀ {S : Set α}, (∀ a, ∃ b ∈ S, r a b) → c ≤ #S :=
by
rw [cof, le_csInf_iff'' (cof_nonempty r)]
use fun H S h => H _ ⟨S, h, rfl⟩
rintro H d ⟨S, h, rfl⟩
exact H h
