Glossary: O

Definitions in this project whose names start with O. The whole glossary has the other sections.

A · B · C · D · E · F · G · H · I · J · K · L · M · N · O · P · Q · R · S · T · U · V · W · X · Y · Z · Other

ObtuseAt def

The angle $yxz$ is obtuse. · Erdos224.ObtuseAt

octahedron abbrev

The octahedron $K_{2,2,2}$: the complete tripartite graph with all three parts of size $2$. · Erdos579.octahedron

oddCycleLengths def

G.oddCycleLengths is the set of lengths of odd cycles in G. · SimpleGraph.oddCycleLengths

OddPrime def

def OddPrime (n : ℕ) : Prop · Lemoine.OddPrime

oeisFloorTerm def

The floor term in the conjectured recurrence relation for A267581. This term, $\lfloor (1/2)^{(2^{n+1} \bmod n)} \rfloor$, simplifies to 1 if $(2^{n+1} \bmod n) = 0$ (i.e., $n \mid 2^{n+1}$), and 0 otherwise. Since the recurrence is only … · OeisA267581.oeisFloorTerm

of def

The class {a} of a unit a in K^M_1(F)/ℓ. · MilnorK.of

ofDigitsMsf def

Convert a list of decimal digits (most significant first) to a natural number. · OeisA87571.ofDigitsMsf

OfDiscrete def

A bijection between discrete topological spaces induces a homeomorphism. · Homeomorph.OfDiscrete

ofEdgeFamily def

A family of finite edges on an explicit vertex set, retaining isolated vertices. · Hypergraph.ofEdgeFamily

OfFiniteOrder def

An entire function f is said to be of finite order if there exist numbers c, a ≥ 0 such that for all z, ‖f z‖ ≤ c * rexp (‖z‖ ^ a). · Erdos516.OfFiniteOrder

ofFinset def

A finite uniform edge family viewed as a uniform hypergraph. · UniformHypergraph.ofFinset

offWalk def

The set of vertices that a walk does not touch. For a longest cycle C this set carries the graph G - V(C) of the conjecture. · Arxiv.«2606.03696».offWalk

ofHom def

The class map {·} : Fˣ → K^M_1(F)/ℓ as an additive homomorphism. · MilnorK.ofHom

ofLeftInverse def

Transport a BitstringEncoding along an injection f with partial inverse g. · BitstringEncoding.ofLeftInverse

ofLeftInverse def

If f : β → α has a left inverse finv such that f ∘ finv is primitive recursive, then β is Primcodable, with b encoded as Encodable.encode (f b). · Primcodable.ofLeftInverse

ofSubtype def

A subtype inherits the encoding of the ambient type; decoding additionally checks the defining predicate. · BitstringEncoding.ofSubtype

ogfAScaled def

The power series $A(x/3) = \sum_{n=0}^\infty \frac{a(n)}{3^n} x^n$ over ℚ. · OeisA228143.ogfAScaled

omega def

$\omega_n = A_n^2 + B_n^2 = \prod_{k=1}^n (1 + k^2)$, the norm of $Z_n$. · Arxiv.«2607.05739».omega

Omega1 abbrev

The set of countable ordinals, expressed using Mathlib's ω_ 1. · Erdos1128.Omega1

omegaGt def

omegaGt k n counts the number of distinct prime factors of n that are strictly greater than k. · Erdos890.omegaGt

omegaIntegral def

For an integer-valued function $\omega$ on the set of primes and a sequence $a_n$ of rational numbers, the condition $\omega$-integrality means that for each prime $p$, the rational numbers $a_0, a_1, \dots, a_{\omega(p)}$ are in … · LamLitt.omegaIntegral

OmegaP def

OmegaP S p counts the number of residue classes mod p where at least one polynomial in S vanishes. · BatemanHornConjecture.OmegaP

omegaSuperlinear def

The growth condition on $\omega$: the ratio $\omega(p) / p$ tends to infinity as the prime $p$ tends to infinity, i.e. $\lim_{p \to \infty} \omega(p) / p = \infty$. Here the source filter is Filter.atTop on the primes, obtained by … · LamLitt.omegaSuperlinear

oneSmoothGL def

The constant function 1 as an element of smoothGL n; the constant functions are the line it spans. · Matrix.GeneralLinearGroup.oneSmoothGL

openLevelSet def

The set $\{ z \in \mathbb{C} : \lvert f(z)\rvert < 1\}$ · Erdos1048.openLevelSet

orderedExpField abbrev

The language of ordered exponential fields: the language of rings, together with a unary function symbol exp and the order relation ≤. · FirstOrder.Language.orderedExpField

orderFourGenerator def

A generator for a circulant Hadamard matrix of order four. · CirculantHadamard.orderFourGenerator

orderIsoIdeal def

Over a commutative semiring, right ideals and ideals are order isomorphic. · RightIdeal.orderIsoIdeal

OrdinalCardinalRamsey def

This proposition asserts the ordinal Ramsey property α → (β, c)². · OrdinalCardinalRamsey

OrdinalCardinalRamsey3 def

OrdinalCardinalRamsey3 α β c asserts the 3-uniform ordinal Ramsey property $\alpha \to (\beta, c)^3_2$. · Erdos70.OrdinalCardinalRamsey3

Orthogonal def

Two latin squares of the same order are orthogonal if superimposing them gives each ordered pair of symbols at most once. · LatinSquare.Orthogonal

orthogonalSubgroup def

The orthogonal group O n ℝ as a subgroup of GL n ℝ: the units of Matrix n n ℝ whose underlying matrix lies in mathlib's Matrix.orthogonalGroup n ℝ, the submonoid of matrices whose transpose is their inverse. This is the maximal … · Matrix.GeneralLinearGroup.orthogonalSubgroup

other def

Returns the other player. · CatchUp.Player.other

Outcome inductive

The possible outcomes of a Catch-Up game. · CatchUp.Outcome

Overlap def

The number of solutions to the equation $a - b = k$, for $a \in A$ and $b \in B$. This represents the "overlap" between sets $A$ and $B$ for a given difference $k$. · Erdos36.Overlap

overlapSq def

The squared magnitude of the overlap between two state vectors. · OpenQuantumProblem23.overlapSq