covBy_iff_atom_Ici — Mathlib

English

If a ≤ b, then CovBy a b holds if and only if ⟨b, h⟩ is an atom in Set.Ici a, where h is the witness a ≤ b.

Русский

Если a ≤ b, то CovBy a b верно тогда, когда ⟨b, h⟩ является атомом в Set.Ici a, где h — доказательство a ≤ b.

LaTeX

$$$ (\\forall h:\\, a \\le b),\\ CovBy\\, a\\, b \\iff \\mathrm{IsAtom}(\\langle b, h \\rangle ).$$$

Lean4

theorem covBy_iff_atom_Ici (h : a ≤ b) : a ⋖ b ↔ IsAtom (⟨b, h⟩ : Set.Ici a) := by simp

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