theorem Nat.monotone_of_succ_monotone {n m : ℕ} {r : ℕ → ℕ → Prop} (rfx : Std.Refl r) (tr : IsTrans ℕ r) (succ : ∀ (n : ℕ), r n (n + 1)) : n ≤ m → r n m

theorem DirectedOn.fintype_colimit {α : Type u_1} {r : α → α → Prop} {ι : Type u_2} [Fintype ι] (tr : IsTrans α r) {s : Set α} (hs : s.Nonempty) (h : DirectedOn r s) (v : ι → α) (hv : ∀ (i : ι), v i ∈ s) : ∃ z ∈ s, ∀ (i : ι), r (v i) z

Compatibility and incompatibility

def Order.IsCompatiblePair {α : Type u_1} [Preorder α] (a b : α) : Prop

Equations

• Order.IsCompatiblePair a b = ∃ c ≤ a, c ≤ b

def Order.«term_‖_» : Lean.TrailingParserDescr

Equations

• Order.«term_‖_» = Lean.ParserDescr.trailingNode `Order.«term_‖_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ‖ ") (Lean.ParserDescr.cat `term 51))

@[simp]

theorem Order.IsCompatiblePair.refl {α : Type u_1} [Preorder α] (a : α) : IsCompatiblePair a a

theorem Order.IsCompatiblePair.symm_iff {α : Type u_1} [Preorder α] {a b : α} : IsCompatiblePair a b ↔ IsCompatiblePair b a

theorem Order.IsCompatiblePair.symm {α : Type u_1} [Preorder α] {a b : α} : IsCompatiblePair a b → IsCompatiblePair b a

Alias of the forward direction of Order.IsCompatiblePair.symm_iff.

theorem Order.IsCompatiblePair.of_le {α : Type u_1} [Preorder α] {a b : α} (h : a ≤ b) : IsCompatiblePair a b

def Order.IsIncompatiblePair {α : Type u_1} [Preorder α] (a b : α) : Prop

Equations

• Order.IsIncompatiblePair a b = ¬Order.IsCompatiblePair a b

def Order.«term_⟂_» : Lean.TrailingParserDescr

Equations

• Order.«term_⟂_» = Lean.ParserDescr.trailingNode `Order.«term_⟂_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⟂ ") (Lean.ParserDescr.cat `term 51))

theorem Order.isIncompatiblePair_iff {α : Type u_1} [Preorder α] {a b : α} : IsIncompatiblePair a b ↔ ∀ c ≤ a, ¬c ≤ b

@[simp]

theorem Order.IsIncompatiblePair.antirefl {α : Type u_1} [Preorder α] (a : α) : ¬IsIncompatiblePair a a

theorem Order.IsIncompatiblePair.symm_iff {α : Type u_1} [Preorder α] {a b : α} : IsIncompatiblePair a b ↔ IsIncompatiblePair b a

theorem Order.IsIncompatiblePair.symm {α : Type u_1} [Preorder α] {a b : α} : IsIncompatiblePair a b → IsIncompatiblePair b a

Alias of the forward direction of Order.IsIncompatiblePair.symm_iff.

theorem Order.IsIncompatiblePair.lower {α : Type u_1} [Preorder α] {a a' b b' : α} (h : IsIncompatiblePair a b) (ha'a : a' ≤ a) (hb'b : b' ≤ b) : IsIncompatiblePair a' b'

@[simp]

theorem Order.not_isCompatiblePair_iff_isIncompatiblePair {α : Type u_1} [Preorder α] {a b : α} : ¬IsCompatiblePair a b ↔ IsIncompatiblePair a b

@[simp]

theorem Order.not_isIncompatiblePair_iff_isCompatiblePair {α : Type u_1} [Preorder α] {a b : α} : ¬IsIncompatiblePair a b ↔ IsCompatiblePair a b

Density

def Order.IsDense {α : Type u_1} [Preorder α] (s : Set α) : Prop

Equations

• Order.IsDense s = ∀ (p : α), ∃ q ≤ p, q ∈ s

def Order.IsDenseBelow {α : Type u_1} [Preorder α] (s : Set α) (a : α) : Prop

Equations

• Order.IsDenseBelow s a = ∀ p ≤ a, ∃ q ≤ p, q ∈ s

structure Order.DenseSet (α : Type u_1) [Preorder α] : Type u_1

• set : Set α
• is_dense : IsDense self.set

theorem Order.DenseSet.ext_iff {α : Type u_1} {inst✝ : Preorder α} {x y : DenseSet α} : x = y ↔ x.set = y.set

theorem Order.DenseSet.ext {α : Type u_1} {inst✝ : Preorder α} {x y : DenseSet α} (set : x.set = y.set) : x = y

@[instance_reducible]

instance Order.DenseSet.instSetLike {α : Type u_1} [Preorder α] : SetLike (DenseSet α) α

Equations

• Order.DenseSet.instSetLike = { coe := fun (s : Order.DenseSet α) => s.set, coe_injective := ⋯ }

noncomputable def Order.DenseSet.choose {α : Type u_1} [Preorder α] (d : DenseSet α) (a : α) : α

Equations

• d.choose a = ⋯.choose

@[simp]

theorem Order.DenseSet.choose_le {α : Type u_1} [Preorder α] (d : DenseSet α) (a : α) : d.choose a ≤ a

@[simp]

theorem Order.DenseSet.choose_mem {α : Type u_1} [Preorder α] (d : DenseSet α) (a : α) : d.choose a ∈ d

def Order.PFilter.ofDescendingChain {α : Type u_1} [Preorder α] (s : ℕ → α) (hs : ∀ (i j : ℕ), i ≤ j → s i ≥ s j) : PFilter α

Equations

• Order.PFilter.ofDescendingChain s hs = ⋯.toPFilter

@[simp]

theorem Order.PFilter.mem_descendingChain_iff {α : Type u_1} [Preorder α] {x : α} (s : ℕ → α) (hs : ∀ (i j : ℕ), i ≤ j → s i ≥ s j) : x ∈ ofDescendingChain s hs ↔ ∃ (i : ℕ), s i ≤ x

class Order.PFilter.IsGeneric {α : Type u_1} [Preorder α] (F : PFilter α) (𝓓 : Set (DenseSet α)) : Prop

• isGeneric (d : DenseSet α) : d ∈ 𝓓 → ∃ a ∈ F, a ∈ d

@[simp]

instance Order.PFilter.IsGeneric.empty {α : Type u_1} [Preorder α] (F : PFilter α) : F.IsGeneric ∅

theorem Order.PFilter.exists_genericFilter_of_countable {α : Type u_1} [Preorder α] (𝓓 : Set (DenseSet α)) (ctb : 𝓓.Countable) (a : α) : ∃ (G : PFilter α), G.IsGeneric 𝓓 ∧ a ∈ G