mem_iff_find_le

Mathlib.Topology.Compactness.SigmaCompact

URI: https://scilib.ai/kg/mathlib#CompactExhaustion.mem_iff_find_le

← MathLib Explorer

English

x ∈ K_n iff K.find x ≤ n (the minimal index ≤ n).

Русский

x ∈ K_n тогда и только тогда, когда K.find x ≤ n (минимальный индекс не больше n).

LaTeX

$$$$x \in K_n \iff K.find x \le n.$$$$

Lean4

theorem mem_iff_find_le {x : X} {n : ℕ} : x ∈ K n ↔ K.find x ≤ n := by
  classical exact ⟨fun h => Nat.find_min' (K.exists_mem x) h, fun h => K.subset h <| K.mem_find x⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru