inf_le — Mathlib

English

For any a, b, c in a semilattice with inf, if a is InfPrime, then b ⊓ c ≤ a iff b ≤ a or c ≤ a.

Русский

В полузаданной структуре с операция inf, если a является InfPrime, то b ⊓ c ≤ a эквивалентно (b ≤ a) или (c ≤ a).

LaTeX

$$$$\\text{InfPrime}(a) \\to \\bigl( b \\sqcap c \\le a \\iff b \\le a \\lor c \\le a \\bigr).$$$$

Lean4

theorem inf_le (ha : InfPrime a) : b ⊓ c ≤ a ↔ b ≤ a ∨ c ≤ a :=
  ⟨fun h => ha.2 h, fun h => h.elim inf_le_of_left_le inf_le_of_right_le⟩

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