Theorems · Theorem · order theory

IsUpperSet.image_fibration

∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : LE α] [inst_1 : LE β],
  Relation.Fibration (fun x1 x2 => x1 ≥ x2) (fun x1 x2 => x1 ≥ x2) f → ∀ {s : Set α}, IsUpperSet s → IsUpperSet (f '' s)

Alias of Relation.Fibration.isUpperSet_image.

Defined in

Mathlib.Order.UpperLower.Fibration

Cited by

1 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

LELE