Theorems · Theorem · order theory

MonotoneOn.csInf_eq_of_subset_of_forall_exists_le

∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : ConditionallyCompleteLattice β] {f : α → β} {s t : Set α},
  BddBelow (f '' t) → MonotoneOn f t → s ⊆ t → (∀ y ∈ t, ∃ x ∈ s, x ≤ y) → sInf (f '' s) = sInf (f '' t)

Defined in

Mathlib.Order.ConditionallyCompleteLattice.Basic

Cited by

1 results in Mathlib

Foundations

Depth 28 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PreorderConditionallyCompleteLattice