Candidate.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.HyperbolicObstruction.BernoulliCandidates.card_lower_of_embeddings line 18
Source documentation
A convenient subset of the actual fieldwise-injective candidates consists of globally injective free values avoiding every pinned letter. This is only a lower bound; the actual candidate set does not prohibit cross-field coincidences.
```
lemma card_lower_of_embeddings (C : Finset (V → A)) (B : Finset A)
    (hC : ∀ f : V ↪ {a : A // a ∉ B}, (fun v => (f v).val) ∈ C) :
    ((Fintype.card A - B.card).descFactorial (Fintype.card V)) ≤ C.card := by
…
```
lemma OAI.HyperbolicObstruction.BernoulliCandidates.real_descFactorial_lower line 34
lemma OAI.HyperbolicObstruction.BernoulliCandidates.card_lower_half line 46