Supporting results for pointwise provable equality.

theorem PointwiseComposition.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 PointwiseComposition.DirectedOn.fintype_colimit {α : Type u_1} {r : α → α → Prop} {ι : Type u_2} [Finite ι] (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 PointwiseComposition.Order.IsCompatiblePair {α : Type u_1} [Preorder α] (a b : α) : Prop

The Is Compatible Pair construction in Order.

Equations

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

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

The «term ‖ » construction in Order.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

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

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

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

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

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

The Is Incompatible Pair construction in Order.

Equations

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

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

The «term ⟂ » construction in Order.

Equations

• One or more equations did not get rendered due to their size.

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

@[simp]

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

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

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

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

theorem PointwiseComposition.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 PointwiseComposition.Order.not_isCompatiblePair_iff_isIncompatiblePair {α : Type u_1} [Preorder α] {a b : α} : ¬IsCompatiblePair a b ↔ IsIncompatiblePair a b

@[simp]

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

Density

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

The Is Dense construction in Order.

Equations

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

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

The Is Dense Below construction in Order.

Equations

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

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

Data and laws for Dense Set in Order.

• set : Set α

  The set construction in Order.DenseSet.

• is_dense : IsDense self.set

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

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

@[instance_reducible]

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

Equations

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

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

The choose construction in Order.DenseSet.

Equations

• d.choose a = ⋯.choose

@[simp]

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

@[simp]

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

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

The of Descending Chain construction in Order.PFilter.

Equations

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

@[simp]

theorem PointwiseComposition.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 PointwiseComposition.Order.PFilter.IsGeneric {α : Type u_1} [Preorder α] (F : Order.PFilter α) (𝓓 : Set (DenseSet α)) : Prop

Data and laws for Is Generic in Order.PFilter.

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

@[simp]

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

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