BourbakiLean2.Order.Monotone

theorem Monotone.comp_anti {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β → γ} {g : α → β} [LE α] [LE β] [LE γ] (h : Monotone f) (h' : Antitone g) :

Antitone (f ∘ g)

source

theorem Monotone.restrict {β : Type u_2} {γ : Type u_3} {f : β → γ} [LE β] [LE γ] {x : Set β} (h : Monotone f) :

Monotone (f|_x)

source

theorem Antitone.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β → γ} {g : α → β} [LE α] [LE β] [LE γ] (h : Antitone f) (h' : Antitone g) :

Monotone (f ∘ g)

source

theorem Antitone.comp_mono {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β → γ} {g : α → β} [LE α] [LE β] [LE γ] (h : Antitone f) (h' : Monotone g) :

Antitone (f ∘ g)

source

theorem Antitone.restrict {β : Type u_2} {γ : Type u_3} {f : β → γ} [LE β] [LE γ] {x : Set β} (h : Antitone f) :

Antitone (f|_x)

source

theorem isOrderIso_iff_reflect {β : Type u_2} {γ : Type u_3} {f : β → γ} [LE β] [LE γ] :

IsOrderIso f ↔ Function.Bijective f ∧ Monotone f ∧ ∀ (x y : β), f x ≤ f y → x ≤ y

source

theorem IsOrderIso.le_iff {β : Type u_2} {γ : Type u_3} {f : β → γ} [LE β] [LE γ] (h : IsOrderIso f) {a b : β} :

f a ≤ f b ↔ a ≤ b

source

theorem IsOrderIso.inv {β : Type u_2} {γ : Type u_3} {f : β → γ} [LE β] [LE γ] (h : IsOrderIso f) :

IsOrderIso ⋯.inv

source

theorem IsOrderIso.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β → γ} {g : α → β} [LE α] [LE β] [LE γ] (h : IsOrderIso f) (h' : IsOrderIso g) :

IsOrderIso (f ∘ g)

source

theorem id_isOrderIso {α : Type u_1} [LE α] :

IsOrderIso id

source

@[simp]

theorem id_strict_mono {α : Type u_1} [LT α] :

StrictMonotone id

source

theorem StrictMonotone.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β → γ} {g : α → β} [LT α] [LT β] [LT γ] (h : StrictMonotone f) (h' : StrictMonotone g) :

StrictMonotone (f ∘ g)

source

theorem StrictMonotone.comp_strictAnti {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β → γ} {g : α → β} [LT α] [LT β] [LT γ] (h : StrictMonotone f) (h' : StrictAntitone g) :

StrictAntitone (f ∘ g)

source

theorem StrictAntitone.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β → γ} {g : α → β} [LT α] [LT β] [LT γ] (h : StrictAntitone f) (h' : StrictAntitone g) :

StrictMonotone (f ∘ g)

source

theorem StrictAntitone.comp_mono {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β → γ} {g : α → β} [LT α] [LT β] [LT γ] (h : StrictAntitone f) (h' : StrictMonotone g) :

StrictAntitone (f ∘ g)

source

theorem StrictMonotone.restrict {β : Type u_2} {γ : Type u_3} {f : β → γ} [LT β] [LT γ] {x : Set β} (h : StrictMonotone f) :

StrictMonotone (f|_x)

source

theorem StrictAntitone.restrict {β : Type u_2} {γ : Type u_3} {f : β → γ} [LT β] [LT γ] {x : Set β} (h : StrictAntitone f) :

StrictAntitone (f|_x)

source

@[simp]

theorem const_mono {α : Type u_1} {β : Type u_2} [LE α] [Preorder β] {b : β} :

Monotone (Function.const α b)

source

@[simp]

theorem const_anti {α : Type u_1} {β : Type u_2} [LE α] [Preorder β] {b : β} :

Antitone (Function.const α b)

source

theorem StrictMonotone.monotone {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {f : α → β} (h : StrictMonotone f) :

Monotone f

source

theorem Monotone.strictMono_of_inj {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {f : α → β} (h : Monotone f) (h' : Function.Injective f) :

StrictMonotone f

source

theorem Antitone.strictAnti_of_inj {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {f : α → β} (h : Antitone f) (h' : Function.Injective f) :

StrictAntitone f

source

@[simp]

theorem toOp_antitone {α : Type u_1} [LE α] :

Antitone toOp

source

@[simp]

theorem toOp_strictAnti {α : Type u_1} [LT α] :

StrictAntitone toOp

source

@[simp]

theorem fromOp_antitone {α : Type u_1} [LE α] :

Antitone fromOp

source

@[simp]

theorem fromOp_strictAnti {α : Type u_1} [LT α] :

StrictAntitone fromOp

source

theorem monotone_iff_toOp_antitone {α : Type u_1} {β : Type u_2} {f : α → β} [LE α] [LE β] :

Monotone f ↔ Antitone (toOp ∘ f)

source

theorem monotone_iff_fromOp_antitone {α : Type u_1} {β : Type u_2} {f : α → β} [LE α] [LE β] :

Monotone f ↔ Antitone (f ∘ fromOp)

source

theorem antitone_iff_toOp_monotone {α : Type u_1} {β : Type u_2} {f : α → β} [LE α] [LE β] :

Antitone f ↔ Monotone (toOp ∘ f)

source

theorem antitone_iff_fromOp_monotone {α : Type u_1} {β : Type u_2} {f : α → β} [LE α] [LE β] :

Antitone f ↔ Monotone (f ∘ fromOp)

source

theorem strictMono_iff_toOp_strictAnti {α : Type u_1} {β : Type u_2} {f : α → β} [LT α] [LT β] :

StrictMonotone f ↔ StrictAntitone (toOp ∘ f)

source

theorem strictMono_iff_fromOp_strictAnti {α : Type u_1} {β : Type u_2} {f : α → β} [LT α] [LT β] :

StrictMonotone f ↔ StrictAntitone (f ∘ fromOp)

source

theorem strictAnti_iff_toOp_strictMono {α : Type u_1} {β : Type u_2} {f : α → β} [LT α] [LT β] :

StrictAntitone f ↔ StrictMonotone (toOp ∘ f)

source

theorem strictAnti_iff_fromOp_strictMono {α : Type u_1} {β : Type u_2} {f : α → β} [LT α] [LT β] :

StrictAntitone f ↔ StrictMonotone (f ∘ fromOp)

source

@[simp]

theorem Set.compl_strictAnti {α : Type u_1} :

StrictAntitone Set.compl

source

theorem pseudoinv_of_antitone {α : Type u_1} {β : Type u_2} [Preorder α] [PartialOrder β] {f : α → β} {g : β → α} (hf : Antitone f) (h : ∀ (x : α), g (f x) ≥ x) (h' : ∀ (y : β), f (g y) ≥ y) :

f ∘ g ∘ f = f

source

theorem Subtype.val_monotone {α : Type u_1} {p : α → Prop} [LE α] :

Monotone Subtype.val

source

theorem Subtype.val_strictMonotone {α : Type u_1} {p : α → Prop} [LT α] :

StrictMonotone Subtype.val

source

theorem PartialMap.carrier_monotone {α : Type u_1} {β : α → Type u_3} :

Monotone PartialMap.carrier

source

theorem IsOrderIso.lt_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} (h : IsOrderIso f) {a b : α} :

f a < f b ↔ a < b

source

theorem IsOrderIso.strictMonotone {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} (h : IsOrderIso f) :

StrictMonotone f