inf_eq_minDefault — Mathlib

English

For α with a semilattice infimum, decidable ≤, and IsTotal ≤, the meet operation coincides with minDefault: ⊓ equals minDefault.

Русский

Пусть α имеет полупорядок с meet, разрешено сравнение ≤ и порядок тотален. Тогда операция meet совпадает с minDefault.

LaTeX

$$$ (\,\sqcap \,) = (\minDefault : α \to α \to α) $$$

Lean4

theorem inf_eq_minDefault [SemilatticeInf α] [DecidableLE α] [IsTotal α (· ≤ ·)] : (· ⊓ ·) = (minDefault : α → α → α) :=
  by
  ext x y
  unfold minDefault
  split_ifs with h'
  exacts [inf_of_le_left h', inf_of_le_right <| (total_of (· ≤ ·) x y).resolve_left h']

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