exists_diff_singleton_of_not_minimal

English

If hP is monotone (for all s,t with t ⊆ s, P t → P s) and hs: P s and h: ¬Minimal P s, then there exists x ∈ s with P (s \\ { x }).

Русский

Если P монотонно по включениям и hs: P s, h: ¬Minimal P s, тогда существует x ∈ s такое, что P (s \\ { x }).

LaTeX

$$$$ (\\forall s,t, P t \\to P s \\text{ при } t \\subset s) \\land (hs : P s) \\land (h : \\neg Minimal P s) \\Longrightarrow \\exists x\\in s, P (s \\setminus \\{x\\}). $$$$

Lean4

theorem exists_diff_singleton_of_not_minimal (hP : ∀ ⦃s t⦄, P t → t ⊆ s → P s) (hs : P s) (h : ¬Minimal P s) :
    ∃ x ∈ s, P (s \ { x }) := by simpa [Set.minimal_iff_forall_diff_singleton hP, hs] using h

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