not_isMin_coe — Mathlib

English

Let J be a ordered set with S ⊆ J. If m ∈ S is not minimal in S, then its projection m.1 in J is not minimal in J.

Русский

Пусть J упорядочено, S ⊆ J. Если m ∈ S не минимален в S, то m.1 не минимален в J.

LaTeX

$$$\forall (J) [\text{Preorder } J] (S : Set J) (m : S.Elem), \neg IsMin m \Rightarrow \neg IsMin m.1$$$

Lean4

theorem not_isMin_coe (hm : ¬IsMin m) : ¬IsMin m.1 := fun h ↦ hm (fun _ hb ↦ h hb)

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