map_inf — Mathlib

English

If f is an order-embedding that is an isomorphism between α and β, then f(x ∧ y) = f(x) ∧ f(y) for all x, y in α.

Русский

Если f — взаимно однозначное вложение порядка между α и β, то для любых x, y в α выполняется f(x ∧ y) = f(x) ∧ f(y).

LaTeX

$$$ f(x \wedge y) = f(x) \wedge f(y) $$$

Lean4

theorem map_inf [SemilatticeInf α] [SemilatticeInf β] (f : α ≃o β) (x y : α) : f (x ⊓ y) = f x ⊓ f y :=
  by
  refine (f.toOrderEmbedding.map_inf_le x y).antisymm ?_
  apply f.symm.le_iff_le.1
  simpa using f.symm.toOrderEmbedding.map_inf_le (f x) (f y)

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