Iic — Mathlib

English

If a is an atom and a ≤ x, then the pair ⟨a, hax⟩ in Set.Iic x is also an atom.

Русский

Если a — атом и a ≤ x, то элемент ⟨a, hax⟩ в Set.Iic x тоже является атомом.

LaTeX

$$$IsAtom(a) \\land a \\le x \\Rightarrow IsAtom\\langle a, hax \\rangle.$$$

Lean4

theorem Iic (ha : IsAtom a) (hax : a ≤ x) : IsAtom (⟨a, hax⟩ : Set.Iic x) :=
  ⟨fun con => ha.1 (Subtype.mk_eq_mk.1 con), fun ⟨b, _⟩ hba => Subtype.mk_eq_mk.2 (ha.2 b hba)⟩

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