candidatesBOfCandidates_mem — Mathlib

English

If f is a candidate for the pair (X, Y) and fA witnesses that f belongs to the candidate set, then the corresponding bound-candidate object lies in the bound-candidates set.

Русский

Если f является кандидатом для пары (X, Y) и fA свидетельствует о том, что f принадлежит множеству кандидатов, то соответствующий элемент ограниченного кандидатов принадлежит множеству ограниченных кандидатов.

LaTeX

$$$candidatesBOfCandidates(f,f_A) \in candidatesB(X,Y)$$$

Lean4

theorem candidatesBOfCandidates_mem (f : ProdSpaceFun X Y) (fA : f ∈ candidates X Y) :
    candidatesBOfCandidates f fA ∈ candidatesB X Y :=
  fA

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