Iic — Mathlib

English

Another variant of the two-parameter supremum interaction with Ici (structurally the same).

Русский

Еще одна вариация взаимодействия двухпараметричной верхней грани и Ici.

LaTeX

$$$Ici\left(\bigvee_i \bigvee_j f(i,j)\right) = \bigvee_i \bigvee_j Ici(f(i,j))$$$

Lean4

/-- Principal lower set. `Set.Iic` as a lower set. The smallest lower set containing a given
element. -/
nonrec def Iic (a : α) : LowerSet α :=
  ⟨Iic a, isLowerSet_Iic a⟩

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