findAtom_eq_bot — Mathlib

English

findAtom r is not bottom exactly when r is not bottom.

Русский

findAtom r ≠ ⊥ тогда и только тогда, когда r ≠ ⊥.

LaTeX

$$findAtom(r) ≠ ⊥ \\Leftrightarrow r ≠ ⊥$$

Lean4

@[simp]
theorem findAtom_eq_bot {r : α} : findAtom r = ⊥ ↔ r = ⊥
    where
  mp
    h := by
    unfold findAtom at h
    have := Nat.find_min' (bot_le (a := r)).exists_pred_iterate h
    replace : Nat.find (bot_le (a := r)).exists_pred_iterate = 0 := by omega
    simpa [this] using h
  mpr h := by simp [h]

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