not_isMax_coe — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem not_isMax_coe (hm : ¬IsMax m) : ¬IsMax m.1 := fun h ↦ hm (fun _ hb ↦ h hb)

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