cof_le — Mathlib

English

For a relation r on α and a witness-set S such that for every a there exists b ∈ S with r a b, cof r ≤ |S|.

Русский

Для отношения r на A и множества-очевидителя S, для которого для каждого a ∃ b ∈ S с r a b, выполняется cof r ≤ |S|.

LaTeX

$$$\\operatorname{cof}(r) \\le |S|$$$

Lean4

theorem cof_le (r : α → α → Prop) {S : Set α} (h : ∀ a, ∃ b ∈ S, r a b) : cof r ≤ #S :=
  csInf_le' ⟨S, h, rfl⟩

Похожие утверждения