IsOfFiniteCharacter — Mathlib

English

A family F of subsets of α has finite character iff for every X, X ∈ F iff every finite subset of X is in F.

Русский

Семейство F подмножеств α имеет конечный характер тогда и только тогда, когда для каждого X верно: X ∈ F тогда и только тогда, когда каждый конечный подмножество Y ⊆ X принадлежит F.

LaTeX

$$$\\text{IsOfFiniteCharacter } F := \\forall x:\\\\ Set α, x \\in F \\iff \\forall y \\subseteq x, y.Finite \\rightarrow y \\in F$$$

Lean4

/-- A family of sets $F$ is of finite character iff for every set $X$, $X ∈ F$ iff every finite
subset of $X$ is in $F$ -/
def IsOfFiniteCharacter :=
  ∀ x, x ∈ F ↔ ∀ y ⊆ x, y.Finite → y ∈ F

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