Skip to content

Instantly share code, notes, and snippets.

View appendix-c.lean
import data.set.finite
import topology.instances.real
open set
def is_maximal {α : Type*} [partial_order α] (s : set α) (b : α) : Prop :=
∃ (h : b ∈ s), ∀ b's, b ≤ b' → b = b'
lemma exists_maximal {α : Type*} [partial_order α] (s : set α) (hs : finite s) :
as, ∃ b (h : a ≤ b), is_maximal s b :=