Theorems · Theorem
List.TFAE.out
∀ {l : List Prop},
l.TFAE →
∀ (n₁ n₂ : ℕ) {a b : Prop},
autoParam (l[n₁]? = some a) List.TFAE.out._auto_1 → autoParam (l[n₂]? = some b) List.TFAE.out._auto_3 → (a ↔ b)- Defined in
- Mathlib.Data.List.TFAE
- Cited by
- 177 results in Mathlib
- Foundations
- Depth 46 from the axioms, rests on 395 definitions · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- List.TFAEstatement and proof · cited by 102
Cited by177
Results whose statement or proof uses this declaration.
- specializes_iff_mem_closureproof · cited by 11
- exists_mem_nhds_isClosed_subsetproof · cited by 9
- tendstoLocallyUniformlyOn_iff_forall_isCompactproof · cited by 8
- Matroid.singleton_depproof · cited by 8
- isNoetherian_iff'proof · cited by 6
- specializes_iff_pureproof · cited by 6
- Algebra.FormallySmooth.comp_surjectiveproof · cited by 6
- RCLike.conj_eq_iff_reproof · cited by 5
- FormalMultilinearSeries.norm_mul_pow_le_mul_pow_of_lt_radiusproof · cited by 5
- mem_nhdsGT_iff_exists_Ioo_subset'proof · cited by 5
- mem_nhdsLT_iff_exists_Ioo_subset'proof · cited by 5
- LinearIsometry.normDet_eq_oneproof · cited by 4