map_sup

Mathlib.Order.Lattice

URI: https://scilib.ai/kg/mathlib#Antitone.map_sup

English

If f is antitone, then f(x ⊔ y) = f x ⊓ f y when half-typed; i.e., the dual property.

Русский

Если f антитонна, то f(x ⊔ y) = f x ⊓ f y в двойственном виде.

LaTeX

$$$ [SemilatticeInf β] {f : \alpha → β} (hf : Antitone f) (x y : \alpha) : f(x \sqcup y) = f x \sqcap f y$$$

Lean4

theorem map_sup [SemilatticeInf β] {f : α → β} (hf : Antitone f) (x y : α) : f (x ⊔ y) = f x ⊓ f y :=
  hf.dual_right.map_sup x y

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru