isMin_coe — Mathlib

English

For a flag element a in α, IsMin((a : α)) is equivalent to IsMin(a) in the flag.

Русский

Для элемента флага a ∈ α, IsMin((a:α)) эквивалентно IsMin(a) внутри флага.

LaTeX

$$$ \\text{IsMin}(a: \\alpha) \\iff \\text{IsMin}(a). $$$

Lean4

@[simp]
theorem isMin_coe : IsMin (a : α) ↔ IsMin a where
  mp h b hba := h hba
  mpr h b
    hba := by
    refine @h ⟨b, mem_iff_forall_le_or_ge.2 fun c hc ↦ ?_⟩ hba
    classical exact .inl <| hba.trans <| h.isBot ⟨c, hc⟩

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